Created
May 22, 2016 22:54
-
-
Save IvantheTricourne/46f0cbfdd7e1f6f5d601a0e636a72f13 to your computer and use it in GitHub Desktop.
A (beginner) Homotopy Type Theory proof: Two definitions of Circles are "homotopy equivalent"
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# OPTIONS --without-K #-} | |
module Circle where | |
open import HoTT | |
open import Level using (_⊔_) | |
open import Data.Product using (Σ; _,_) | |
open import Function | |
-- Proof: | |
-- Higher inductive type (Circle 1) | |
module Circle1 where | |
private | |
data S¹* : Set where | |
base* : S¹* | |
S¹ : Set | |
S¹ = S¹* | |
base : S¹ | |
base = base* | |
postulate | |
loop : base ≡ base | |
recS¹ : {C : Set} → (cbase : C) → (cloop : cbase ≡ cbase) → S¹ → C | |
recS¹ cbase cloop base* = cbase | |
postulate | |
βrecS¹ : {C : Set} → (cbase : C) → (cloop : cbase ≡ cbase) → | |
ap (recS¹ cbase cloop) loop ≡ cloop | |
indS¹ : {C : S¹ → Set} → | |
(cbase : C base) → (cloop : transport C loop cbase ≡ cbase) → | |
(circle : S¹) → C circle | |
indS¹ cbase cloop base* = cbase | |
postulate | |
βindS¹ : {C : S¹ → Set} → | |
(cbase : C base) → (cloop : transport C loop cbase ≡ cbase) → | |
apd (indS¹ {C} cbase cloop) loop ≡ cloop | |
open Circle1 public | |
-- Higher inductive type (Circle 2) | |
module Circle2 where | |
private | |
data S¹'* : Set where | |
south* : S¹'* | |
north* : S¹'* | |
S¹' : Set | |
S¹' = S¹'* | |
south : S¹' | |
south = south* | |
north : S¹' | |
north = north* | |
postulate | |
east : south ≡ north | |
west : south ≡ north | |
recS¹' : {C : Set} → | |
(csouth cnorth : C) → (ceast cwest : csouth ≡ cnorth) → S¹' → C | |
recS¹' csouth cnorth ceast cwest south* = csouth | |
recS¹' csouth cnorth ceast cwest north* = cnorth | |
postulate | |
βreceastS¹' : {C : Set} → | |
(csouth cnorth : C) → (ceast cwest : csouth ≡ cnorth) → | |
ap (recS¹' csouth cnorth ceast cwest) east ≡ ceast | |
βrecwestS¹' : {C : Set} → | |
(csouth cnorth : C) → (ceast cwest : csouth ≡ cnorth) → | |
ap (recS¹' csouth cnorth ceast cwest) west ≡ cwest | |
indS¹' : {C : S¹' → Set} → | |
(csouth : C south) → (cnorth : C north) → | |
(ceast : transport C east csouth ≡ cnorth) → | |
(cwest : transport C west csouth ≡ cnorth) → | |
(circle : S¹') → C circle | |
indS¹' csouth cnorth ceast cwest south* = csouth | |
indS¹' csouth cnorth ceast cwest north* = cnorth | |
postulate | |
βindeastS¹' : {C : S¹' → Set} → | |
(csouth : C south) → (cnorth : C north) → | |
(ceast : transport C east csouth ≡ cnorth) → | |
(cwest : transport C west csouth ≡ cnorth) → | |
apd (indS¹' {C} csouth cnorth ceast cwest) east ≡ ceast | |
βindwestS¹' : {C : S¹' → Set} → | |
(csouth : C south) → (cnorth : C north) → | |
(ceast : transport C east csouth ≡ cnorth) → | |
(cwest : transport C west csouth ≡ cnorth) → | |
apd (indS¹' {C} csouth cnorth ceast cwest) west ≡ cwest | |
open Circle2 public | |
-- take base to north, | |
-- take loop around the entire S¹' circle | |
f : S¹ → S¹' | |
f = recS¹ north (! east · west) | |
-- take north, south to base | |
-- take west to loop, take east to refl | |
g : S¹' → S¹ | |
g = recS¹' base base (refl base) loop | |
-- theorem 2-11-3 | |
2-11-3 : {A B : Set} (f g : A → B) {a a' : A} (p : a ≡ a') (q : f a ≡ g a) → | |
transport (λ x → f x ≡ g x) p q ≡ ! (ap f p) · q · (ap g p) | |
2-11-3 f g {a} {a'} p q = | |
pathInd (λ {a a'} p → (q : f a ≡ g a) → | |
transport (λ x → f x ≡ g x) p q ≡ ! (ap f p) · q · (ap g p)) | |
(λ a q → | |
q ≡⟨ unitTransR q ⟩ | |
q · (refl $ g a) ≡⟨ unitTransL $ q · (refl $ g a) ⟩ | |
(refl $ f a) · q · (refl $ g a) ∎) | |
{a} {a'} p q | |
-- homotopy 1 : (x : S¹) → g (f x) ≡ x | |
βcircle : (g ∘ f) ∼ id | |
βcircle = indS¹ (refl base) cloop where | |
cloop = transport (λ z → (g ∘ f) z ≡ id z) loop (refl base) | |
≡⟨ 2-11-3 (g ∘ f) id loop (refl base) ⟩ | |
! (ap (g ∘ f) loop) · refl base · (ap id loop) | |
≡⟨ ap (λ x → ! (ap (g ∘ f) loop) · refl base · x) (apfId loop) ⟩ | |
! (ap (g ∘ f) loop) · refl base · loop | |
≡⟨ ap (λ x → ! x · refl base · loop) (! (apfComp f g loop)) ⟩ | |
! (ap g (ap f loop)) · refl base · loop | |
≡⟨ ap (λ x → ! (ap g x) · refl base · loop) (βrecS¹ north (! east · west)) ⟩ | |
! (ap g (! east · west)) · refl base · loop | |
≡⟨ ap (λ x → ! x · refl base · loop) (apfTrans g (! east) west) ⟩ | |
! (ap g (! east) · ap g west) · refl base · loop | |
≡⟨ ap (λ x → ! (ap g (! east) · x) · refl base · loop) (βrecwestS¹' base base (refl base) loop) ⟩ | |
! (ap g (! east) · loop) · refl base · loop | |
≡⟨ ap (λ x → ! (x · loop) · refl base · loop) (apfInv g east) ⟩ | |
! (! (ap g east) · loop) · refl base · loop | |
≡⟨ ap (λ x → ! (! x · loop) · refl base · loop) (βreceastS¹' base base (refl base) loop) ⟩ | |
! (! (refl base) · loop) · refl base · loop | |
≡⟨ ap (λ x → x · refl base · loop) (invComp (! $ refl base) loop) ⟩ | |
(! loop · ! (! $ refl base)) · refl base · loop | |
≡⟨ ap (λ x → (! loop · x) · refl base · loop) (invId $ refl base) ⟩ | |
(! loop · refl base) · refl base · loop | |
≡⟨ ap (λ x → (! loop · refl base) · x) (! $ unitTransL loop) ⟩ | |
(! loop · refl base) · loop | |
≡⟨ ! $ assocP (! loop) (refl base) loop ⟩ | |
! loop · (refl base · loop) | |
≡⟨ ap (λ x → ! loop · x) (! $ unitTransL loop) ⟩ | |
! loop · loop | |
≡⟨ invTransL loop ⟩ | |
refl base | |
∎ | |
-- homotopy 2 : (x : S¹') → f (g x) ≡ x | |
βcircle' : (f ∘ g) ∼ id | |
βcircle' = indS¹' (! east) (refl north) ceast cwest where | |
ceast = transport (λ z → (f ∘ g) z ≡ id z) east (! east) | |
≡⟨ 2-11-3 (f ∘ g) id east (! east) ⟩ | |
! (ap (f ∘ g) east) · ! east · (ap id east) | |
≡⟨ ap (λ x → ! (ap (f ∘ g) east) · ! east · x) (apfId east) ⟩ | |
! (ap (f ∘ g) east) · ! east · east | |
≡⟨ ap (λ x → ! x · ! east · east) (! (apfComp g f east)) ⟩ | |
! (ap f (ap g east)) · ! east · east | |
≡⟨ ap (λ x → ! (ap f x) · ! east · east) (βreceastS¹' base base (refl base) loop) ⟩ | |
! (ap f (refl base)) · ! east · east | |
≡⟨ ap (λ x → ! (ap f (refl base)) · x) (invTransL east) ⟩ | |
! (ap f (refl base)) · refl north | |
≡⟨ refl (refl north) ⟩ | |
refl north | |
∎ | |
cwest = transport (λ z → (f ∘ g) z ≡ id z) west (! east) | |
≡⟨ 2-11-3 (f ∘ g) id west (! east) ⟩ | |
! (ap (f ∘ g) west) · ! east · (ap id west) | |
≡⟨ ap (λ x → ! (ap (f ∘ g) west) · ! east · x) (apfId west) ⟩ | |
! (ap (f ∘ g) west) · ! east · west | |
≡⟨ ap (λ x → ! x · ! east · west) (! (apfComp g f west)) ⟩ | |
! (ap f (ap g west)) · ! east · west | |
≡⟨ ap (λ x → ! (ap f x) · ! east · west) (βrecwestS¹' base base (refl base) loop) ⟩ | |
! (ap f loop) · ! east · west | |
≡⟨ ap (λ x → ! x · ! east · west) (βrecS¹ north (! east · west)) ⟩ | |
! (! east · west) · ! east · west | |
≡⟨ ap (λ x → x · ! east · west) (invComp (! east) west) ⟩ | |
(! west · ! (! east)) · ! east · west | |
≡⟨ ap (λ x → (! west · x) · ! east · west) (invId east) ⟩ | |
(! west · east) · ! east · west | |
≡⟨ assocP (! west · east) (! east) west ⟩ | |
((! west · east) · ! east) · west | |
≡⟨ ap (λ x → x · west) (! $ assocP (! west) east (! east)) ⟩ | |
(! west · (east · ! east)) · west | |
≡⟨ ap (λ x → (! west · x) · west) (invTransR east) ⟩ | |
(! west · refl south) · west | |
≡⟨ ! $ assocP (! west) (refl south) west ⟩ | |
! west · (refl south · west) | |
≡⟨ ap (λ x → ! west · x) (! $ unitTransL west) ⟩ | |
! west · west | |
≡⟨ invTransL west ⟩ | |
refl north | |
∎ | |
sequiv : S¹ ≃ S¹' | |
sequiv = f , mkisequiv g βcircle' g βcircle | |
spath : S¹ ≡ S¹' | |
spath with univalence | |
... | (_ , eq) = isequiv.g eq sequiv | |
------------------------------------------------------------------------------ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# OPTIONS --without-K #-} | |
-- Everything you need to do homotopy type theory in Agda | |
module HoTT where | |
open import Level using (_⊔_) | |
open import Data.Product using (Σ; _,_) | |
open import Function | |
infixr 8 _·_ -- path composition | |
infix 4 _≡_ -- propositional equality | |
infix 4 _∼_ -- homotopy between two functions | |
infix 4 _≃_ -- type of equivalences | |
------------------------------------------------------------------------------ | |
-- A few HoTT primitives | |
data _≡_ {ℓ} {A : Set ℓ} : (a b : A) → Set ℓ where | |
refl : (a : A) → (a ≡ a) | |
pathInd : ∀ {u ℓ} → {A : Set u} → | |
(C : {x y : A} → x ≡ y → Set ℓ) → | |
(c : (x : A) → C (refl x)) → | |
({x y : A} (p : x ≡ y) → C p) | |
pathInd C c (refl x) = c x | |
-- | |
! : ∀ {u} → {A : Set u} {x y : A} → (x ≡ y) → (y ≡ x) | |
! = pathInd (λ {x} {y} _ → y ≡ x) refl | |
_·_ : ∀ {u} → {A : Set u} → {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z) | |
_·_ {u} {A} {x} {y} {z} p q = | |
pathInd {u} | |
(λ {x} {y} p → ((z : A) → (q : y ≡ z) → (x ≡ z))) | |
(λ x z q → pathInd (λ {x} {z} _ → x ≡ z) refl {x} {z} q) | |
{x} {y} p z q | |
_≡⟨_⟩_ : ∀ {ℓ} {A : Set ℓ} (x : A) {y : A} → x ≡ y → {z : A} → y ≡ z → x ≡ z | |
_ ≡⟨ p ⟩ q = p · q | |
infixr 2 _≡⟨_⟩_ | |
_∎ : ∀ {ℓ} {A : Set ℓ} → (x : A) → x ≡ x | |
x ∎ = refl x | |
infixl 3 _∎ | |
-- | |
unitTransR : {A : Set} {x y : A} → (p : x ≡ y) → (p ≡ p · refl y) | |
unitTransR {A} {x} {y} p = | |
pathInd | |
(λ {x} {y} p → p ≡ p · (refl y)) | |
(λ x → refl (refl x)) | |
{x} {y} p | |
unitTransL : {A : Set} {x y : A} → (p : x ≡ y) → (p ≡ refl x · p) | |
unitTransL {A} {x} {y} p = | |
pathInd | |
(λ {x} {y} p → p ≡ (refl x) · p) | |
(λ x → refl (refl x)) | |
{x} {y} p | |
invTransL : {A : Set} {x y : A} → (p : x ≡ y) → (! p · p ≡ refl y) | |
invTransL {A} {x} {y} p = | |
pathInd | |
(λ {x} {y} p → ! p · p ≡ refl y) | |
(λ x → refl (refl x)) | |
{x} {y} p | |
invTransR : ∀ {ℓ} {A : Set ℓ} {x y : A} → (p : x ≡ y) → (p · ! p ≡ refl x) | |
invTransR {ℓ} {A} {x} {y} p = | |
pathInd | |
(λ {x} {y} p → p · ! p ≡ refl x) | |
(λ x → refl (refl x)) | |
{x} {y} p | |
invId : {A : Set} {x y : A} → (p : x ≡ y) → (! (! p) ≡ p) | |
invId {A} {x} {y} p = | |
pathInd | |
(λ {x} {y} p → ! (! p) ≡ p) | |
(λ x → refl (refl x)) | |
{x} {y} p | |
assocP : {A : Set} {x y z w : A} → (p : x ≡ y) → (q : y ≡ z) → (r : z ≡ w) → | |
(p · (q · r) ≡ (p · q) · r) | |
assocP {A} {x} {y} {z} {w} p q r = | |
pathInd | |
(λ {x} {y} p → (z : A) → (w : A) → (q : y ≡ z) → (r : z ≡ w) → | |
p · (q · r) ≡ (p · q) · r) | |
(λ x z w q r → | |
pathInd | |
(λ {x} {z} q → (w : A) → (r : z ≡ w) → | |
(refl x) · (q · r) ≡ ((refl x) · q) · r) | |
(λ x w r → | |
pathInd | |
(λ {x} {w} r → | |
(refl x) · ((refl x) · r) ≡ | |
((refl x) · (refl x)) · r) | |
(λ x → (refl (refl x))) | |
{x} {w} r) | |
{x} {z} q w r) | |
{x} {y} p z w q r | |
invComp : {A : Set} {x y z : A} → (p : x ≡ y) → (q : y ≡ z) → | |
! (p · q) ≡ ! q · ! p | |
invComp {A} {x} {y} {z} p q = | |
pathInd | |
(λ {x} {y} p → (z : A) → (q : y ≡ z) → ! (p · q) ≡ ! q · ! p) | |
(λ x z q → | |
pathInd | |
(λ {x} {z} q → ! (refl x · q) ≡ ! q · ! (refl x)) | |
(λ x → refl (refl x)) | |
{x} {z} q) | |
{x} {y} p z q | |
-- | |
ap : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : Set ℓ'} {x y : A} → | |
(f : A → B) → (x ≡ y) → (f x ≡ f y) | |
ap {ℓ} {ℓ'} {A} {B} {x} {y} f p = | |
pathInd | |
(λ {x} {y} p → f x ≡ f y) | |
(λ x → refl (f x)) | |
{x} {y} p | |
apfTrans : ∀ {u} → {A B : Set u} {x y z : A} → | |
(f : A → B) → (p : x ≡ y) → (q : y ≡ z) → ap f (p · q) ≡ (ap f p) · (ap f q) | |
apfTrans {u} {A} {B} {x} {y} {z} f p q = | |
pathInd {u} | |
(λ {x} {y} p → (z : A) → (q : y ≡ z) → | |
ap f (p · q) ≡ (ap f p) · (ap f q)) | |
(λ x z q → | |
pathInd {u} | |
(λ {x} {z} q → | |
ap f (refl x · q) ≡ (ap f (refl x)) · (ap f q)) | |
(λ x → refl (refl (f x))) | |
{x} {z} q) | |
{x} {y} p z q | |
apfInv : ∀ {u} → {A B : Set u} {x y : A} → (f : A → B) → (p : x ≡ y) → | |
ap f (! p) ≡ ! (ap f p) | |
apfInv {u} {A} {B} {x} {y} f p = | |
pathInd {u} | |
(λ {x} {y} p → ap f (! p) ≡ ! (ap f p)) | |
(λ x → refl (ap f (refl x))) | |
{x} {y} p | |
apfComp : {A B C : Set} {x y : A} → (f : A → B) → (g : B → C) → (p : x ≡ y) → | |
ap g (ap f p) ≡ ap (g ∘ f) p | |
apfComp {A} {B} {C} {x} {y} f g p = | |
pathInd | |
(λ {x} {y} p → ap g (ap f p) ≡ ap (g ∘ f) p) | |
(λ x → refl (ap g (ap f (refl x)))) | |
{x} {y} p | |
apfId : {A : Set} {x y : A} → (p : x ≡ y) → ap id p ≡ p | |
apfId {A} {x} {y} p = | |
pathInd | |
(λ {x} {y} p → ap id p ≡ p) | |
(λ x → refl (refl x)) | |
{x} {y} p | |
-- | |
transport : ∀ {ℓ ℓ'} → {A : Set ℓ} {x y : A} → | |
(P : A → Set ℓ') → (p : x ≡ y) → P x → P y | |
transport {ℓ} {ℓ'} {A} {x} {y} P p = | |
pathInd -- on p | |
(λ {x} {y} p → (P x → P y)) | |
(λ _ → id) | |
{x} {y} p | |
apd : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : A → Set ℓ'} {x y : A} → (f : (a : A) → B a) → | |
(p : x ≡ y) → (transport B p (f x) ≡ f y) | |
apd {ℓ} {ℓ'} {A} {B} {x} {y} f p = | |
pathInd | |
(λ {x} {y} p → transport B p (f x) ≡ f y) | |
(λ x → refl (f x)) | |
{x} {y} p | |
-- Homotopies and equivalences | |
_∼_ : ∀ {ℓ ℓ'} → {A : Set ℓ} {P : A → Set ℓ'} → | |
(f g : (x : A) → P x) → Set (ℓ ⊔ ℓ') | |
_∼_ {ℓ} {ℓ'} {A} {P} f g = (x : A) → f x ≡ g x | |
record qinv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) : | |
Set (ℓ ⊔ ℓ') where | |
constructor mkqinv | |
field | |
g : B → A | |
α : (f ∘ g) ∼ id | |
β : (g ∘ f) ∼ id | |
record isequiv {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) : | |
Set (ℓ ⊔ ℓ') where | |
constructor mkisequiv | |
field | |
g : B → A | |
α : (f ∘ g) ∼ id | |
h : B → A | |
β : (h ∘ f) ∼ id | |
equiv₁ : ∀ {ℓ ℓ'} → {A : Set ℓ} {B : Set ℓ'} {f : A → B} → qinv f → isequiv f | |
equiv₁ (mkqinv qg qα qβ) = mkisequiv qg qα qg qβ | |
_≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ') | |
A ≃ B = Σ (A → B) isequiv | |
postulate | |
univalence : {A B : Set} → (A ≡ B) ≃ (A ≃ B) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment