Investigations on graph-theoretical constructions in Homotopy type theory

{-# OPTIONS --without-K --exact-split #-}

module foundations.HedbergLemmas where

open import foundations.TransportLemmas
open import foundations.EquivalenceType
open import foundations.HLevelTypes
open import foundations.RelationType
open import foundations.FunExtAxiom
open import foundations.FunExtTransport

module
  HedbergLemmas
  where
  module
    HedbergLemmas2
    where

A set is a type when it holds Axiom K.

axiomKisSet
  : ∀ {ℓ : Level} {A : Type ℓ}
  → ((a : A) → (p : a ≡ a) → p ≡ refl a)
  → isSet A

axiomKisSet k x _ p idp = k x p

reflRelIsSet
  : ∀ {ℓ : Level} (A : Type ℓ)
  → (r : Rel A)
  → ((x y : A) → R {{r}} x y → x ≡ y)  -- xRy ⇒ Id(x,y)
  →   ((x : A) → R {{r}} x x)           -- ∀ x ⇒ xRx
  ------------------------------------
  → isSet A

reflRelIsSet A r f ρ x .x p idp = lemma p
  where
  lemma2
    : {a : A}
    → (p : a ≡ a) → (o : R {{r}} a a)
    → (f a a o) ≡ f a a (transport (R {{r}} a) p o)
                 [ (λ x → a ≡ x) ↓ p ]

  lemma2 {a} p = funext-transport-l p (f a a) (f a a) (apd (f a) p)

  lemma3
    :  {a : A}
    → (p : a ≡ a)
    → (f a a (ρ a)) · p ≡ (f a a (ρ a))

  lemma3 {a} p = inv (transport-concat-r p _) · lemma2 p (ρ a) ·
                   ap (f a a) (Rprop {{r}} a a _ (ρ a))

  lemma
    : {a : A}
    → (p : a ≡ a)
    → p ≡ refl a

  lemma {a} p = ·-cancellation ((f a a (ρ a))) p (lemma3 p)

Lema: if a type is decidable, then ¬¬A is actually A.

lemDoubleNeg
  : ∀ {ℓ : Level} {A : Type ℓ}
  → (A + ¬ A)
  ---------------
  → (¬ (¬ A) → A)

lemDoubleNeg (inl x) _ = x
lemDoubleNeg (inr f) n = exfalso (n f)

hedberg
  : ∀ {ℓ : Level} {A : Type ℓ}
  → ((a b : A) → (a ≡ b) + ¬ (a ≡ b))
  -----------------------------------
  → isSet A

hedberg {ℓ}{A = A} f
  = reflRelIsSet A
      (record { R = λ a b → ¬ (¬ (a ≡ b))
              ; Rprop = isPropNeg })
              doubleNegEq (λ a z → z (refl a))

  where
  doubleNegEq
   : (a b : A) → ¬ (¬ (a ≡ b))
   → (a ≡ b)

  doubleNegEq a b p = lemDoubleNeg (f a b) p

  isPropNeg
    : (a b : A)
    → isProp (¬ (¬ (a ≡ b)))

  isPropNeg a b x y = funext λ u → exfalso (x u)

More syntax:

decidable-is-set = hedberg

Latest changes

(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides
(2022-07-06)(d3a4a8cf) minors by jonathan.cubides
(2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides
(2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides
(2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides
(2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides
(2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides
(2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides
(2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides
(2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides
(2021-12-15)(0630ce66) Minor fixes by jonathan.cubides
(2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides
(2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides
(2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides
(2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides