Skip to content

Instantly share code, notes, and snippets.

@cheery
Created February 9, 2023 16:36
Show Gist options
  • Save cheery/3bade79072e3b43e16d23bfcebb58477 to your computer and use it in GitHub Desktop.
Save cheery/3bade79072e3b43e16d23bfcebb58477 to your computer and use it in GitHub Desktop.
Hedberg's theorem
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment