Hedberg's theorem

hedberg.agda

{-# OPTIONS --cubical #-}
module hedberg where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws

data Empty : Set where

absurd : {A : Set} → Empty → A
absurd ()

_∘_ : {A B C : Set} → (B → C) → (A → B) → A → C
(f ∘ g) x = f (g x)

id : {A : Set} → A → A
id x = x

pcong : {A B : Set} → {x y : A} → {f g : A → B} → (f ≡ g) → (f x ≡ f y) → (g x ≡ g y)
pcong {x = x} {y = y} f≡g = transp (λ i → f≡g i x ≡ f≡g i y) i0

data ∥_∥ (A : Set) : Set where
  ∣_∣ : A → ∥ A ∥
  squash : (x y : ∥ A ∥) → x ≡ y

-- ∥ X ∥ → X  iff constant endomap is available

hprop : Set → Set
hprop X = (x y : X) → x ≡ y

h-set : Set → Set
h-set X =  (x y : X) → hprop (x ≡ y)

data decidable (A : Set) : Set where
  yes : A → decidable A
  no : (A → Empty) → decidable A

discrete : Set → Set
discrete X = (x y : X) → decidable (x ≡ y)

constant : {X Y : Set} → (X → Y) → Set
constant {X} f = (x y : X) → f x ≡ f y

collapsible : Set → Set
collapsible X = Σ[ f ∈ (X → X) ] constant f

path-collapsible : Set → Set
path-collapsible X = (x y : X) → collapsible (x ≡ y)

discrete→path-collapsible : {X : Set}
                          → discrete X → path-collapsible X
discrete→path-collapsible {X} d x y
  = map , cm
  where map : x ≡ y → x ≡ y
        map x≡y with d x y
        map x≡y | yes x≡y' = x≡y'
        map x≡y | no f = absurd (f x≡y)
        cm : constant map
        cm p q with d x y
        cm p q | yes x = (λ i → x)
        cm p q | no x = absurd (x p)

path-collapsible→h-set : {X : Set}
                       → path-collapsible X → h-set X
path-collapsible→h-set {X} pc x y p q = pcong lif (cong g (snd (pc x y) p q))
   where g : x ≡ y → x ≡ y
         g x≡y = x≡y ∙ sym (fst (pc y y) refl)
         lif : g ∘ (fst (pc x y)) ≡ id
         lif i x≡y = J (λ y x≡y → fst (pc x y) x≡y ∙ sym (fst (pc y y) refl) ≡ x≡y)
                       (rCancel (fst (pc x x) refl))
                       x≡y i

-- Hedberg's theorem
discrete→h-set : {X : Set} → discrete X → h-set X
discrete→h-set d = path-collapsible→h-set (discrete→path-collapsible d)

stable : Set → Set
stable X = ((X → Empty) → Empty) → X

separated : Set → Set
separated X = (x y : X) → stable (x ≡ y)

separated→h-set : {X : Set} → separated X → h-set X
separated→h-set {X} sep = path-collapsible→h-set λ x y → (sep x y ∘ obvious x y) , c x y
  where obvious : (x y : X) → (x ≡ y) → ((x ≡ y → Empty) → Empty)
        obvious x y x≡y f = f x≡y
        lemma : {X : Set} (p q : X → Empty) → (x : X) → p x ≡ q x
        lemma p q x = absurd (p x)
        lemma₂ : {X : Set} (p q : X → Empty) → p ≡ q
        lemma₂ p q i x = lemma p q x i
        c : (x y : X) → constant (sep x y ∘ obvious x y)
        c x y x≡y₁ x≡y₂ i j = sep x y (lemma₂ (obvious x y x≡y₁) (obvious x y x≡y₂) i) j

cong-preserves-constant : {A B : Set} → {f : A → B} {x y : A}
                       → constant f → constant (cong {x = x} {y = y} f)
cong-preserves-constant {f = f} {x = x} {y = y} cf p q = lemma p ∙ sym (lemma q)
  where lemma : ∀ p → cong {x = x} {y = y} f p ≡ sym (cf x x) ∙ cf x y
        lemma = J (λ y x≡y → cong {x = x} {y = y} f x≡y ≡ sym (cf x x) ∙ cf x y)
                  (sym (lCancel (cf x x)))

cong-constant : {A : Set} {B : Set} {f : A → B} {x : A} {x≡x : x ≡ x}
             → constant f
             → cong f x≡x ≡ refl
cong-constant {f = f} {x} {x≡x} c = cong-preserves-constant c _ _

fixed-point-lemma : {X : Set} (f : X → X) → constant f
                 → hprop (Σ[ x ∈ X ] x ≡ f x)
fixed-point-lemma {X} f cf (x , x≡fx) (y , y≡fy) = cong₂ (_,_) x≡fx eq1
                                                 ∙ cong₂ (_,_) (cf x y) eq2
                                                 ∙ cong₂ (_,_) (sym y≡fy) eq3
  where transport' : {X Y : Set} → (h k : X → Y)
              → {x y : X} → (t : x ≡ y) → (p : h x ≡ k x) → h y ≡ k y
        transport' h k t p = sym (cong h t) ∙ p ∙ cong k t
        x≡y : x ≡ y
        x≡y = x≡fx ∙ cf x y ∙ sym y≡fy
        x≡x : x ≡ x
        x≡x = x≡fx ∙ sym (subst (λ z → z ≡ f z) (sym x≡y) y≡fy)
        fx≡ffx : f x ≡ f (f x)
        fx≡ffx = cong f x≡fx
        fy≡ffy : f y ≡ f (f y)
        fy≡ffy = cong f y≡fy
        fx≡ffy : f x ≡ f (f y)
        fx≡ffy = cong f (x≡fx ∙ cf x y)
        eq1 : PathP (λ i → x≡fx i ≡ f (x≡fx i)) x≡fx fx≡ffx
        eq1 i j = hfill (λ k → λ{(i = i0) → x≡fx j
                                 ;(i = i1) → fx≡ffx k
                                 ;(j = i1) → f (x≡fx (i ∧ k))}) (inS (x≡fx (i ∨ j))) j
        eq2 : PathP (λ i → cf x y i ≡ f (cf x y i)) fx≡ffx fy≡ffy
        eq2 i j = {!!}
        eq3 : PathP (λ i → y≡fy (~ i) ≡ f (y≡fy (~ i))) fy≡ffy y≡fy
        eq3 i j = hfill (λ k → λ{(i = i0) → fy≡ffy (j ∧ k)
                                 ;(i = i1) → y≡fy j
                                 ;(j = i1) → f (y≡fy (~ i ∧ k))}) (inS (y≡fy (j ∨ (~ i)))) j