Imports
{-# OPTIONS --rewriting #-} module HottBook.Chapter2 where open import Agda.Primitive.Cubical hiding (i1) open import HottBook.Chapter1 open import HottBook.Chapter1Util open import HottBook.Chapter2Lemma221 public open import HottBook.Chapter2Lemma231 public open import HottBook.Chapter2Definition217 public private variable l l2 : Level
2 Homotopy type theory
2.1 Types are higher groupoids
Lemma 2.1.1
sym : {l : Level} {A : Set l} {x y : A} → (x ≡ y) → y ≡ x sym {l} {A} {x} {y} refl = refl
Lemma 2.1.2
trans : {l : Level} {A : Set l} {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z) trans {l} {A} {x} {y} {z} refl refl = refl infixr 30 _∙_ _∙_ = trans
Equational Reasoning
module ≡-Reasoning where infix 1 begin_ begin_ : {l : Level} {A : Set l} {x y : A} → (x ≡ y) → (x ≡ y) begin x = x _≡⟨⟩_ : {l : Level} {A : Set l} (x {y} : A) → x ≡ y → x ≡ y _ ≡⟨⟩ x≡y = x≡y infixr 2 _≡⟨⟩_ step-≡ step-≡ : {l : Level} {A : Set l} (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z step-≡ _ y≡z x≡y = trans x≡y y≡z syntax step-≡ x y≡z x≡y = x ≡⟨ x≡y ⟩ y≡z infix 3 _∎ _∎ : {l : Level} {A : Set l} (x : A) → (x ≡ x) _ ∎ = refl
Lemma 2.1.4
module lemma2∙1∙4 {l : Level} {A : Set l} where i1 : {x y : A} (p : x ≡ y) → p ≡ p ∙ refl i1 {x} {y} refl = refl i2 : {x y : A} (p : x ≡ y) → p ≡ refl ∙ p i2 {x} {y} refl = refl ii1 : {x y : A} (p : x ≡ y) → (sym p) ∙ p ≡ refl ii1 {x} {y} refl = refl ii2 : {x y : A} (p : x ≡ y) → p ∙ (sym p) ≡ refl ii2 {x} {y} refl = refl iii : {x y : A} (p : x ≡ y) → sym (sym p) ≡ p iii {x} {y} refl = refl iv : {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r iv {x} {y} {z} {w} refl refl refl = refl
Theorem 2.1.6 (Eckmann-Hilton)
-- module theorem2∙1∙6 where -- Ω-type : (A : Set) → (a : A) → Set -- Ω-type A a = refl {x = a} ≡ refl -- compose1 : {A : Set} {a : A} → fst (Ω (A , a)) → fst (Ω (A , a)) → fst (Ω (A , a)) -- compose1 x y = x ∙ y -- Ω² : {l : Level} → Set* l → Set* l -- Ω² {l} = Ω[_] {l = l} 2 -- compose2 : {l : Level} {A : Set l} {a : A} → fst (Ω² (A , a)) → fst (Ω² (A , a)) → fst (Ω² (A , a)) -- compose2 x y = horiz x y -- where -- variable -- A : Set l -- a b c : A -- p q : a ≡ b -- r s : b ≡ c -- α : p ≡ q -- β : r ≡ s -- _∙ᵣ_ : p ≡ q → (r : b ≡ c) → p ∙ r ≡ q ∙ r -- α ∙ᵣ refl = sym (lemma2∙1∙4.i1 _) ∙ α ∙ lemma2∙1∙4.i1 _ -- _∙ₗ_ : (q : a ≡ b) → r ≡ s → q ∙ r ≡ q ∙ s -- refl ∙ₗ β = sym (lemma2∙1∙4.i2 _) ∙ β ∙ lemma2∙1∙4.i2 _ -- horiz : p ≡ q → r ≡ s → p ∙ r ≡ q ∙ s -- horiz α β = (α ∙ᵣ _) ∙ (_ ∙ₗ β) -- compose2-commutative : {l : Level} {A : Set l} {a : A} (x y : fst (Ω² (A , a))) → compose2 x y ≡ compose2 y x -- compose2-commutative {l} {A} {a} x y = {! !}
Definition 2.1.7 (pointed type)
Set* : (l : Level) → Set (lsuc l) Set* l = Σ (Set l) (λ A → A)
Definition 2.1.8 (loop space)
Ω : {l : Level} → Set* l → Set* l Ω (A , a) = (a ≡ a) , refl Ω[_] : {l : Level} → ℕ → Set* l → Set* l Ω[ zero ] (A , a) = (A , a) Ω[ suc n ] (A , a) = Ω[ n ] (Ω (A , a))
2.2 Functions are functors
Lemma 2.2.1
ap : {l1 l2 : Level} {A : Set l1} {B : Set l2} {x y : A} → (f : A → B) → (p : x ≡ y) → f x ≡ f y ap {l1} {l2} {A} {B} {x} {y} f p = J (λ x y p → f x ≡ f y) (λ x → refl) x y p
Lemma 2.2.2
Ap rules
module lemma2∙2∙2 where private variable A B C : Set i : {f : A → B} {x y z : A} (p : x ≡ y) (q : y ≡ z) → ap f (p ∙ q) ≡ ap f p ∙ ap f q i {f} {x} {y} {z} refl refl = refl ii : {f : A → B} {x y : A} (p : x ≡ y) → ap f (sym p) ≡ sym (ap f p) ii {f} {x} {y} refl = refl iii : (f : A → B) (g : B → C) {x y : A} (p : x ≡ y) → ap g (ap f p) ≡ ap (g ∘ f) p iii f g {x} {y} refl = refl iv : {x y : A} (p : x ≡ y) → ap id p ≡ p iv {x} {y} refl = refl
2.3 Type families are fibrations
transport : {l₁ l₂ : Level} {A : Set l₁} {x y : A} → (P : A → Set l₂) → (p : x ≡ y) → P x → P y transport {l₁} {l₂} {A} {x} {y} P refl = id
Lemma 2.3.2 (Path lifting property)
module lemma2∙3∙2 where lift : {A : Set} {P : A → Set} {x y : A} → (u : P x) → (p : x ≡ y) → (x , u) ≡ (y , transport P p u) lift {A} {P} {x} {y} u refl = refl pr₁ : {A : Set} {P : A → Set} {x y : A} {u : P x} {v : P y} (p : (x , u) ≡ (y , v)) → x ≡ y pr₁ p = ap (λ (x , y) → x) p open ≡-Reasoning lift-prop : {A : Set} {P : A → Set} {x y : A} (u : P x) → (p : x ≡ y) → pr₁ (lift {A} {P} u p) ≡ p lift-prop {A} {P} {x} {y} u refl = refl
Lemma 2.3.4 (Dependent map)
apd : {l₁ l₂ : Level} {A : Set l₁} {P : A → Set l₂} {x y : A} → (f : (x : A) → P x) → (p : x ≡ y) → transport P p (f x) ≡ f y apd {l₁} {l₂} {A} {P} {x} {y} f refl = refl
Lemma 2.3.5
transportconst : {l₁ l₂ : Level} {A : Set l₁} {x y : A} → (B : Set l₂) → (p : x ≡ y) → (b : B) → transport (λ _ → B) p b ≡ b transportconst {l₁} {l₂} {A} {x} {y} B refl b = refl {-# REWRITE transportconst #-}
Equation 2.3.6
equation2∙3∙6 : {A B : Set} {x y : A} {p : x ≡ y} {f : A → B} → f x ≡ f y → transport (λ _ → B) p (f x) ≡ f y equation2∙3∙6 {A} {B} {x} {y} {p} {f} q = transportconst B p (f x) ∙ q
Equation 2.3.7
equation2∙3∙7 : {A B : Set} {x y : A} {p : x ≡ y} {f : A → B} → transport (λ _ → B) p (f x) ≡ f y → f x ≡ f y equation2∙3∙7 {A} {B} {x} {y} {p} {f} q = sym (transportconst B p (f x)) ∙ q
Lemma 2.3.8
lemma2∙3∙8 : {l : Level} {A B : Set l} → (f : A → B) → {x y : A} → (p : x ≡ y) → apd f p ≡ transportconst B p (f x) ∙ ap f p lemma2∙3∙8 {l} {A} {B} f {x} {y} refl = refl
Lemma 2.3.9
lemma2∙3∙9 : {A : Set} → {x y z : A} → (P : A → Set) → (p : x ≡ y) → (q : y ≡ z) → (u : P x) → transport P q (transport P p u) ≡ transport P (p ∙ q) u lemma2∙3∙9 {A} {x} {y} {z} P refl refl u = refl
Lemma 2.3.10
lemma2∙3∙10 : {l1 l2 : Level} {A B : Set l1} → (f : A → B) → (P : B → Set l2) → {x y : A} → (p : x ≡ y) → (u : P (f x)) → transport (P ∘ f) p u ≡ transport P (ap f p) u lemma2∙3∙10 {l} {A} {B} f P {x} {y} refl u = refl
Lemma 2.3.11
lemma2∙3∙11 : {A : Set} {P Q : A → Set} → (f : (x : A) → P x → Q x) → {x y : A} (p : x ≡ y) → (u : P x) → transport Q p (f x u) ≡ f y (transport P p u) lemma2∙3∙11 {A} {P} {Q} f {x} {y} refl u = refl
2.4 Homotopies and equivalences
Definition 2.4.1 (Homotopy)
infixl 18 _∼_ _∼_ : {l₁ l₂ : Level} {A : Set l₁} {P : A → Set l₂} → (f g : (x : A) → P x) → Set (l₁ ⊔ l₂) _∼_ {l₁} {l₂} {A} {P} f g = (x : A) → f x ≡ g x
Lemma 2.4.2
Homotopy forms an equivalence relation:
∼-refl : {A : Set} {P : A → Set} → (f : (x : A) → P x) → f ∼ f ∼-refl f x = refl ∼-sym : {A : Set} {P : A → Set} → {f g : (x : A) → P x} → f ∼ g → g ∼ f ∼-sym {f} {g} f∼g x = sym (f∼g x) ∼-trans : {l : Level} {A : Set l} {P : A → Set l} → {f g h : (x : A) → P x} → f ∼ g → g ∼ h → f ∼ h ∼-trans {l} {A} {P} {f} {g} {h} f∼g g∼h x = f∼g x ∙ g∼h x
Lemma 2.4.3
lemma2∙4∙3 : {A B : Set} {f g : A → B} (H : f ∼ g) {x y : A} (p : x ≡ y) → H x ∙ ap g p ≡ ap f p ∙ H y lemma2∙4∙3 {A} {B} {f} {g} H {x} {y} refl = let open ≡-Reasoning in begin H x ∙ ap g refl ≡⟨⟩ H x ∙ refl ≡⟨ sym (lemma2∙1∙4.i1 (H x)) ⟩ H x ≡⟨ lemma2∙1∙4.i2 (H x) ⟩ refl ∙ H x ≡⟨⟩ ap f refl ∙ H x ∎
Corollary 2.4.4
-- corollary2∙4∙4 : {A : Set} {f : A → A} {H : f ∼ id} -- → (x : A) -- → H (f x) ≡ ap f (H x) -- corollary2∙4∙4 {A} {f} {H} x = -- let g p = H x in -- -- let naturality = lemma2∙4∙3 H x in -- {! !}
Definition 2.4.6
record qinv {l1 l2 : Level} {A : Set l1} {B : Set l2} (f : A → B) : Set (l1 ⊔ l2) where constructor mkQinv field g : B → A α : (f ∘ g) ∼ id β : (g ∘ f) ∼ id
Example 2.4.7
id-qinv : {l : Level} {A : Set l} → qinv {l} {l} {A} {A} id id-qinv = mkQinv id (λ _ → refl) (λ _ → refl)
Example 2.4.8
module example2∙4∙8 where i : {A : Set} → {x y z : A} → (p : x ≡ y) → qinv (p ∙_) i {A} {x} {y} {z} p = mkQinv g forward backward where g = (sym p) ∙_ forward : (_∙_ p ∘ g) ∼ id forward q = lemma2∙1∙4.iv p (sym p) q ∙ ap (_∙ q) (lemma2∙1∙4.ii2 p) ∙ sym (lemma2∙1∙4.i2 q) backward : (q : y ≡ z) → sym p ∙ (p ∙ q) ≡ q backward q = lemma2∙1∙4.iv (sym p) p q ∙ ap (_∙ q) (lemma2∙1∙4.ii1 p) ∙ sym (lemma2∙1∙4.i2 q) ii : {A : Set} → {x y z : A} → (p : x ≡ y) → qinv (_∙ p) ii {A} {x} {y} {z} p = mkQinv g forward backward where g : z ≡ y → z ≡ x g = _∙ (sym p) forward : (_∙ p ∘ g) ∼ id forward q = sym (lemma2∙1∙4.iv q (sym p) p) ∙ ap (q ∙_) (lemma2∙1∙4.ii1 p) ∙ sym (lemma2∙1∙4.i1 q) backward : (g ∘ _∙ p) ∼ id backward q = sym (lemma2∙1∙4.iv q p (sym p)) ∙ ap (q ∙_) (lemma2∙1∙4.ii2 p) ∙ sym (lemma2∙1∙4.i1 q)
Example 2.4.9
transport-qinv : {A : Set} → {x y : A} → (P : A → Set) → (p : x ≡ y) → qinv (transport P p) transport-qinv P p = mkQinv (transport P (sym p)) (λ py → let wtf = lemma2∙3∙9 P (sym p) p py in trans wtf (ap (λ x → transport P x py) (lemma2∙1∙4.ii1 p))) (λ px → let wtf = lemma2∙3∙9 P p (sym p) px in trans wtf (ap (λ x → transport P x px) (lemma2∙1∙4.ii2 p)))
Definition 2.4.10
record isequiv {l1 l2 : Level} {A : Set l1} {B : Set l2} (f : A → B) : Set (l1 ⊔ l2) where eta-equality constructor mkIsEquiv field g : B → A g-id : (f ∘ g) ∼ id h : B → A h-id : (h ∘ f) ∼ id
qinv-to-isequiv : {l1 l2 : Level} {A : Set l1} {B : Set l2} → {f : A → B} → qinv f → isequiv f qinv-to-isequiv (mkQinv g α β) = mkIsEquiv g α g β
Still kinda shaky on this one, TODO study it later:
isequiv-to-qinv : {l : Level} {A B : Set l} → {f : A → B} → isequiv f → qinv f isequiv-to-qinv {l} {A} {B} {f} (mkIsEquiv g g-id h h-id) = let γ : g ∼ h γ x = (sym (h-id (g x))) ∙ ap h (g-id x) β : (g ∘ f) ∼ id β x = γ (f x) ∙ h-id x in mkQinv g g-id β
Definition 2.4.11
_≃_ : {l1 l2 : Level} → (A : Set l1) (B : Set l2) → Set (l1 ⊔ l2) A ≃ B = Σ[ f ∈ (A → B) ] (isequiv f)
Lemma 2.4.12
module lemma2∙4∙12 where id-equiv : {l : Level} → (A : Set l) → A ≃ A id-equiv A = id , e where e : isequiv id e = mkIsEquiv id (λ _ → refl) id (λ _ → refl) sym-equiv : {A B : Set l} → (f : A ≃ B) → B ≃ A sym-equiv {A} {B} (f , eqv) = let (mkQinv g α β) = isequiv-to-qinv eqv in g , qinv-to-isequiv (mkQinv f β α) trans-equiv : {A B C : Set l} → (f : A ≃ B) → (g : B ≃ C) → A ≃ C trans-equiv {l} {A} {B} {C} (f , f-eqv) (g , g-eqv) = let (mkQinv f-inv f-inv-left f-inv-right) = isequiv-to-qinv f-eqv (mkQinv g-inv g-inv-left g-inv-right) = isequiv-to-qinv g-eqv open ≡-Reasoning forward : ((g ∘ f) ∘ (f-inv ∘ g-inv)) ∼ id forward c = begin ((g ∘ f) ∘ (f-inv ∘ g-inv)) c ≡⟨ ap (λ f → f c) (composite-assoc (f-inv ∘ g-inv) f g) ⟩ (g ∘ (f ∘ f-inv) ∘ g-inv) c ≡⟨ ap g (f-inv-left (g-inv c)) ⟩ (g ∘ id ∘ g-inv) c ≡⟨⟩ (g ∘ g-inv) c ≡⟨ g-inv-left c ⟩ id c ∎ backward : ((f-inv ∘ g-inv) ∘ (g ∘ f)) ∼ id backward a = begin ((f-inv ∘ g-inv) ∘ (g ∘ f)) a ≡⟨ ap (λ f → f a) (composite-assoc (g ∘ f) g-inv f-inv) ⟩ (f-inv ∘ (g-inv ∘ (g ∘ f))) a ≡⟨ ap f-inv (g-inv-right (f a)) ⟩ (f-inv ∘ (id ∘ f)) a ≡⟨⟩ (f-inv ∘ f) a ≡⟨ f-inv-right a ⟩ id a ∎ in g ∘ f , qinv-to-isequiv (mkQinv (f-inv ∘ g-inv) forward backward)
≃-Reasoning
module ≃-Reasoning where infix 1 begin_ begin_ : {l : Level} {A B : Set l} → (A ≃ B) → (A ≃ B) begin x = x _≃⟨⟩_ : {l : Level} (A {B} : Set l) → A ≃ B → A ≃ B _ ≃⟨⟩ x≃y = x≃y infixr 2 _≃⟨⟩_ step-≃ step-≃ : {l : Level} (A {B C} : Set l) → B ≃ C → A ≃ B → A ≃ C step-≃ _ y≃z x≃y = lemma2∙4∙12.trans-equiv x≃y y≃z syntax step-≃ x y≃z x≃y = x ≃⟨ x≃y ⟩ y≃z infix 3 _∎ _∎ : {l : Level} (A : Set l) → (A ≃ A) A ∎ = lemma2∙4∙12.id-equiv A
2.5 The higher groupoid structure of type formers
Definition 2.5.1
definition2∙5∙1 : {B C : Set} {b b' : B} {c c' : C} → ((b , c) ≡ (b' , c')) ≃ ((b ≡ b') × (c ≡ c')) definition2∙5∙1 {B = B} {C = C} {b = b} {b' = b'} {c = c} {c' = c'} = f , qinv-to-isequiv (mkQinv g forward backward) where f : {b b' : B} {c c' : C} → ((b , c) ≡ (b' , c')) → ((b ≡ b') × (c ≡ c')) f p = ap fst p , ap snd p g : {b b' : B} {c c' : C} → ((b ≡ b') × (c ≡ c')) → ((b , c) ≡ (b' , c')) g (refl , refl) = refl forward : {b b' : B} {c c' : C} → (f {b} {b'} {c} {c'} ∘ g {b} {b'} {c} {c'}) ∼ id forward (refl , refl) = refl backward : {b b' : B} {c c' : C} → (g {b} {b'} {c} {c'} ∘ f {b} {b'} {c} {c'}) ∼ id backward refl = refl
2.6 Cartesian product types
Definition 2.6.1
definition2∙6∙1 : {A B : Set l} {x y : A × B} → (p : x ≡ y) → (fst x ≡ fst y) × (snd x ≡ snd y) definition2∙6∙1 p = ap fst p , ap snd p
Theorem 2.6.2
module theorem2∙6∙2 where private variable A B : Set l x y : A × B pair-≡ : (fst x ≡ fst y) × (snd x ≡ snd y) → x ≡ y pair-≡ (refl , refl) = refl backward : ((definition2∙6∙1 {A = A} {B = B} {x = x} {y = y}) ∘ pair-≡) ∼ id backward (refl , refl) = refl forward : (pair-≡ ∘ (definition2∙6∙1 {A = A} {B = B} {x = x} {y = y})) ∼ id forward refl = refl theorem2∙6∙2 : isequiv (definition2∙6∙1 {A = A} {B = B} {x = x} {y = y}) theorem2∙6∙2 = qinv-to-isequiv (mkQinv pair-≡ backward forward) pair-≃ : {A B : Set l} {x y : A × B} → (x ≡ y) ≃ ((fst x ≡ fst y) × (snd x ≡ snd y)) pair-≃ = definition2∙6∙1 , theorem2∙6∙2 open theorem2∙6∙2 using (pair-≡)
Theorem 2.6.4
theorem2∙6∙4 : {Z : Set} {A B : Z → Set} {z w : Z} → (p : z ≡ w) → (x : A z × B z) → transport (λ z → A z × B z) p x ≡ (transport A p (Σ.fst x) , transport B p (Σ.snd x)) theorem2∙6∙4 {Z} {A} {B} {z} {w} refl x = refl
Theorem 2.6.5
theorem2∙6∙5 : {A A' B B' : Set} {g : A → A'} {h : B → B'} → (x y : A × B) → (p : Σ.fst x ≡ Σ.fst y) → (q : Σ.snd x ≡ Σ.snd y) → let f : A × B → A' × B' f z = (g (Σ.fst z) , h (Σ.snd z)) in ap f (pair-≡ (p , q)) ≡ pair-≡ (ap g p , ap h q) theorem2∙6∙5 x y refl refl = refl
2.7 Σ-types
Theorem 2.7.2
Suppose that P : A → U is a type family over a type A and let w, w′ : ∑(x:A) P(x). Then there is an equivalence
theorem2∙7∙2 : {l : Level} {A : Set l} {P : A → Set l} → ((w @ (w1 , w2)) (w' @ (w'1 , w'2)) : Σ A P) → (w ≡ w') ≃ Σ (w1 ≡ w'1) (λ p → transport P p w2 ≡ w'2) theorem2∙7∙2 {l} {A} {P} (w @ (w1 , w2)) (w' @ (w'1 , w'2)) = f , qinv-to-isequiv (mkQinv g forwards backwards) where f : (w ≡ w') → Σ (w1 ≡ w'1) (λ p → transport P p w2 ≡ w'2) f refl = refl , refl g : Σ (w1 ≡ w'1) (λ p → transport P p w2 ≡ w'2) → (w ≡ w') g (refl , refl) = refl forwards : (f ∘ g) ∼ id forwards (refl , refl) = refl backwards : (g ∘ f) ∼ id backwards refl = refl
Corollary 2.7.3
For z : ∑(x:A) P(x), we have z = (pr1(z), pr2(z)).
corollary2∙7∙3 : {A : Set} {P : A → Set} → (z @ (a , b) : Σ A P) → z ≡ (a , b) corollary2∙7∙3 z = refl
Theorem 2.7.4
-- module theorem2∙7∙4 where -- private -- TF = λ P Q x → Σ (P x) (λ u → Q (x , u)) -- theorem2∙7∙4 : {A : Set} {P : A → Set} -- → (Q : Σ A P → Set) -- → {x y : A} -- → (p : x ≡ y) -- → (u z : Σ (P x) (λ u → Q (x , u))) -- → transport (λ r → Σ {! !} {! !}) p (u , z) ≡ (transport {! !} p u , transport {! TF P Q !} (pair-≡ (p , refl)) z) -- theorem2∙7∙4 Q refl u z = refl
2.8 The unit type
Theorem 2.8.1
theorem2∙8∙1 : (x y : 𝟙) → (x ≡ y) ≃ 𝟙 theorem2∙8∙1 x y = func x y , equiv x y where func : (x y : 𝟙) → (x ≡ y) → 𝟙 func x y _ = tt rev : (x y : 𝟙) → 𝟙 → (x ≡ y) rev tt tt _ = refl backwards : (x y : 𝟙) → (func x y ∘ rev x y) ∼ id backwards tt tt tt = refl forwards : (x y : 𝟙) → (rev x y ∘ func x y) ∼ id forwards tt tt refl = refl equiv : (x y : 𝟙) → isequiv (func x y) equiv x y = record { g = rev x y ; g-id = backwards x y ; h = rev x y ; h-id = forwards x y }
2.9 Π-types and the function extensionality axiom
Lemma 2.9.1
postulate lemma2∙9∙1 : {A : Set} {B : A → Set} → (f g : (x : A) → B x) → (f ≡ g) ≃ ((x : A) → f x ≡ g x)
Lemma 2.9.2
happly : {A : Set l} {B : A → Set l2} → {f g : (x : A) → B x} → (p : f ≡ g) → (x : A) → f x ≡ g x happly {A} {B} {f} {g} p x = ap (λ h → h x) p
Axiom 2.9.3 (Function extensionality)
module axiom2∙9∙3 where private variable A : Set l B : A → Set l2 f g : (x : A) → B x postulate funext : ((x : A) → f x ≡ g x) → f ≡ g propositional-computation : (h : (x : A) → f x ≡ g x) → happly (funext h) ≡ h propositional-uniqueness : (p : f ≡ g) → funext (happly p) ≡ p happly-isequiv : isequiv (happly {l} {l2} {A} {B} {f} {g}) happly-isequiv = qinv-to-isequiv (mkQinv funext propositional-computation propositional-uniqueness) happly-equiv : (f ≡ g) ≃ ((x : A) → f x ≡ g x) happly-equiv = happly , happly-isequiv
Equation 2.9.4
equation2∙9∙4 : {l1 l2 : Level} {X : Set l1} {x1 x2 : X} → {A B : X → Set l2} → (f : A x1 → B x1) → (p : x1 ≡ x2) → transport (λ x → A x → B x) p f ≡ λ x → transport B p (f (transport A (sym p) x)) equation2∙9∙4 {l1} {l2} {X} {x1} {x2} {A} {B} f refl = refl
Equation 2.9.5
module equation2∙9∙5 {X : Set} {x1 x2 : X} where Π : (A : X → Set) → (B : (x : X) → A x → Set) → X → Set Π A B x = (a : A x) → B x a hat : {A : X → Set} → (B : (x : X) → A x → Set) → (Σ X A) → Set hat B (fst , snd) = B fst snd --- I have no idea where this goes but this definitely needs to exist pair-≡-d : {A : Set} {B : A → Set} {a1 a2 : A} {b1 : B a1} {b2 : B a2} → (p : a1 ≡ a2) → (transport B p b1 ≡ b2) → (a1 , b1) ≡ (a2 , b2) pair-≡-d refl refl = refl equation2∙9∙5 : (A : X → Set) → (B : (x : X) → A x → Set) → (f : (a : A x1) → B x1 a) → (p : x1 ≡ x2) → (a : A x2) → transport (Π A B) p f a ≡ transport (hat B) (sym (pair-≡-d (sym p) refl)) (f (transport A (sym p) a)) equation2∙9∙5 A B f refl a = refl
Lemma 2.9.6
-- module lemma2∙9∙6 where -- P : (x : X) → Set -- P x = A x → B x -- lemma2∙9∙6 : (p : x ≡ y) -- → (f : A x → B x) -- → (g : A y → B y) -- → (transport P p f ≡ g) ≃ ((a : A x) → transport B p (f a) ≡ g (transport A p a)) -- lemma2∙9∙6 p f g = func , qinv-to-isequiv (mkQinv {! !} {! !} {! !}) -- where -- func : (transport P p f ≡ g) → (a : A x) → transport B p (f a) ≡ g (transport A p a) -- func p1 a = J (λ x y p' → {! !} ≡ y (transport A {! !} a)) {! !} (transport P p f) g p1
2.10 Universes and the univalence axiom
Lemma 2.10.1
idtoeqv : {A B : Set l} → (A ≡ B) → (A ≃ B) idtoeqv refl = transport id refl , qinv-to-isequiv (mkQinv id id-homotopy id-homotopy) where id-homotopy : (id ∘ id) ∼ id id-homotopy x = refl
Axiom 2.10.3 (Univalence)
module axiom2∙10∙3 where private variable A B : Set l postulate ua : (A ≃ B) → (A ≡ B) propositional-computation : (f : A ≃ B) → idtoeqv (ua f) ≡ f propositional-uniqueness : (p : A ≡ B) → p ≡ ua (idtoeqv p) ua-eqv : {A B : Set l} → (A ≃ B) ≃ (A ≡ B) ua-eqv = ua , qinv-to-isequiv (mkQinv idtoeqv (λ p → sym (propositional-uniqueness p)) (λ e → propositional-computation e)) open axiom2∙10∙3
Lemma 2.10.5
-- lemma2∙10∙5 : {l : Level} {A : Set l} {B : A → Set l} -- → (x y : A) -- → (p : x ≡ y) -- → (u : B x) -- → transport B p u ≡ transport id (ap B p) u
2.11 Identity Type
Theorem 2.11.1
-- theorem2∙11∙1 : {A B : Set} -- → (eqv @ (f , f-eqv) : A ≃ B) -- → (a a' : A) -- → (a ≡ a') ≃ (f a ≡ f a') -- theorem2∙11∙1 (f , f-eqv) a a' = -- let -- open ≡-Reasoning -- mkQinv g α β = isequiv-to-qinv f-eqv -- inv : (f a ≡ f a') → a ≡ a' -- inv p = (sym (β a)) ∙ (ap g p) ∙ (β a') -- backward : (p : f a ≡ f a') → (ap f ∘ inv) p ≡ id p -- backward q = begin -- ap f ((sym (β a)) ∙ (ap g q) ∙ (β a')) ≡⟨ lemma2∙2∙2.i (sym (β a)) (ap g q ∙ β a') ⟩ -- ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {! !} ⟩ -- ap f (sym (β a)) ∙ ap f ((ap g q) ∙ (β a')) ≡⟨ {! !} ⟩ -- id q ∎ -- forward : (p : a ≡ a') → (inv ∘ ap f) p ≡ id p -- forward p = begin -- (sym (β a)) ∙ (ap g (ap f p)) ∙ (β a') ≡⟨ ap (λ p → (sym (β a)) ∙ p ∙ (β a')) (lemma2∙2∙2.iii f g p) ⟩ -- (sym (β a)) ∙ (ap (g ∘ f) p) ∙ (β a') ≡⟨ {! !} ⟩ -- -- (sym (β a)) ∙ (ap id p) ∙ (β a') ≡⟨ {! !} ⟩ -- id p ∎ -- eqv = mkQinv inv backward forward -- in -- ap f , qinv-to-isequiv eqv
Lemma 2.11.2
module lemma2∙11∙2 where open ≡-Reasoning i : {l : Level} {A : Set l} {a x1 x2 : A} → (p : x1 ≡ x2) → (q : a ≡ x1) → transport (λ y → a ≡ y) p q ≡ q ∙ p i {l} {A} {a} {x1} {x2} refl refl = refl ii : {l : Level} {A : Set l} {a x1 x2 : A} → (p : x1 ≡ x2) → (q : x1 ≡ a) → transport (λ y → y ≡ a) p q ≡ sym p ∙ q ii {l} {A} {a} {x1} {x2} refl refl = refl iii : {l : Level} {A : Set l} {a x1 x2 : A} → (p : x1 ≡ x2) → (q : x1 ≡ x1) → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p iii refl q = let a = i1 q b = i2 q in b ∙ ap (refl ∙_) a where open lemma2∙1∙4
Theorem 2.11.3
theorem2∙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 ≡ sym (ap f p) ∙ q ∙ (ap g p) theorem2∙11∙3 {A} {B} {f} {g} {a} {a'} refl q = let helper = ap (λ p → sym refl ∙ p) (lemma2∙1∙4.i1 q) in lemma2∙1∙4.i2 q ∙ helper
Theorem 2.11.4
theorem2∙11∙4 : {A : Set} {B : A → Set} {f g : (x : A) → B x} {a a' : A} → (p : a ≡ a') → (q : f a ≡ g a) → transport (λ x → f x ≡ g x) p q ≡ sym (apd f p) ∙ ap (transport B p) q ∙ apd g p theorem2∙11∙4 {A} {B} {f} {g} {a} {a'} refl q = let open ≡-Reasoning q2 = ap id q q≡q2 : q ≡ q2 q≡q2 = J (λ a b p → p ≡ ap id p) (λ x → refl) (f a) (g a) q in begin transport (λ z → f z ≡ g z) refl q ≡⟨⟩ q ≡⟨ q≡q2 ⟩ q2 ≡⟨ (let helper = ap (λ p → refl ∙ p) (lemma2∙1∙4.i1 q2) in lemma2∙1∙4.i2 q2 ∙ helper) ⟩ refl ∙ ap (transport B refl) q ∙ refl ∎
Theorem 2.11.5
-- theorem2∙11∙5 : {A : Set} {a a' : A} -- → (p : a ≡ a') -- → (q : a ≡ a) -- → (r : a' ≡ a') -- → (transport (λ y → y ≡ y) p q ≡ r) ≃ (q ∙ p ≡ p ∙ r) -- theorem2∙11∙5 refl q r = f , qinv-to-isequiv (mkQinv g {! !} {! !}) -- where -- f : q ≡ r → q ∙ refl ≡ refl ∙ r -- f p = sym (lemma2∙1∙4.i1 q) ∙ p ∙ lemma2∙1∙4.i2 r -- g : q ∙ refl ≡ refl ∙ r → id q ≡ r -- g p = (lemma2∙1∙4.i1 q) ∙ p ∙ sym (lemma2∙1∙4.i2 r) -- -- forward : (f ∘ g) ∼ id
2.12 Coproducts
Theorem 2.12.5
module theorem2∙12∙5 {A B : Set l} (a₀ : A) where open import HottBook.CoreUtil using (Lift) code : A + B → Set l code (inl a) = a₀ ≡ a code (inr b) = Lift ⊥ encode : (x : A + B) → (p : inl a₀ ≡ x) → code x encode x p = transport code p refl decode : (x : A + B) → code x → inl a₀ ≡ x decode (inl x) c = ap inl c backward : (x : A + B) → (c : code x) → encode x (decode x c) ≡ c backward (inl x) c = let open ≡-Reasoning in begin encode (inl x) (decode (inl x) c) ≡⟨⟩ transport code (ap inl c) refl ≡⟨ sym (lemma2∙3∙10 inl code c refl) ⟩ transport (λ a → a₀ ≡ a) c refl ≡⟨ lemma2∙11∙2.i c refl ⟩ refl ∙ c ≡⟨ sym (lemma2∙1∙4.i2 c) ⟩ c ∎ forward : (x : A + B) → (p : inl a₀ ≡ x) → decode x (encode x p) ≡ p forward x p = based-path-induction (inl a₀) (λ x1 p1 → decode x1 (encode x1 p1) ≡ p1) refl x p theorem2∙12∙5 : (x : A + B) → (inl a₀ ≡ x) ≃ (code x) theorem2∙12∙5 x = encode x , qinv-to-isequiv (mkQinv (decode x) (backward x) (forward x))
Remark 2.12.6
module remark2∙12∙6 where true≢false : true ≢ false true≢false p = genBot tt where Bmap : 𝟚 → Set Bmap true = 𝟙 Bmap false = ⊥ genBot : 𝟙 → ⊥ genBot = transport Bmap p
2.13 Natural numbers
Theorem 2.13.1
For all we have .
module theorem2∙13∙1 where open ≡-Reasoning code : ℕ → ℕ → Set code zero zero = 𝟙 code zero (suc y) = ⊥ code (suc x) zero = ⊥ code (suc x) (suc y) = code x y r : (n : ℕ) → code n n r zero = tt r (suc n) = r n encode : (m n : ℕ) → m ≡ n → code m n encode m n p = transport (code m) p (r m) decode : (m n : ℕ) → code m n → m ≡ n decode zero zero tt = refl decode (suc m) (suc n) c = ap suc (decode m n c) backward : (m n : ℕ) → (c : code m n) → encode m n (decode m n c) ≡ c backward zero zero tt = refl backward (suc m) (suc n) c = begin encode (suc m) (suc n) (decode (suc m) (suc n) c) ≡⟨⟩ encode (suc m) (suc n) (ap suc (decode m n c)) ≡⟨⟩ transport (code (suc m)) (ap suc (decode m n c)) (r (suc m)) ≡⟨ sym (lemma2∙3∙10 suc (code (suc m)) (decode m n c) (r (suc m))) ⟩ transport (λ n → code (suc m) (suc n)) (decode m n c) (r (suc m)) ≡⟨⟩ transport (code m) (decode m n c) (r m) ≡⟨⟩ encode m n (decode m n c) ≡⟨ backward m n c ⟩ c ∎ forward : (m n : ℕ) → (p : m ≡ n) → decode m n (encode m n p) ≡ p forward m n refl = f m where f : (x : ℕ) → decode x x (r x) ≡ refl f zero = refl f (suc x) = ap (ap suc) (f x) theorem2∙13∙1 : (m n : ℕ) → (m ≡ n) ≃ code m n theorem2∙13∙1 m n = encode m n , qinv-to-isequiv (mkQinv (decode m n) (backward m n) (forward m n))
2.14 Example: equality of structures
Definition 2.14.1
SemigroupStr : (A : Set l) → Set l SemigroupStr A = Σ (A → A → A) (λ m → (x y z : A) → m x (m y z) ≡ m (m x y) z) Semigroup : Set (lsuc l) Semigroup {l = l} = Σ (Set l) SemigroupStr
2.15 Universal properties
Definition 2.15.1
definition2∙15∙1 : {X A B : Set} → (X → A × B) → (X → A) × (X → B) definition2∙15∙1 f = Σ.fst ∘ f , Σ.snd ∘ f
Theorem 2.15.2
theorem2∙15∙2 : {X A B : Set} → isequiv (definition2∙15∙1 {X} {A} {B}) theorem2∙15∙2 {X} {A} {B} = mkIsEquiv g (λ _ → refl) g (λ _ → refl) where g : (X → A) × (X → B) → (X → A × B) g (f1 , f2) = λ x → (f1 x , f2 x)
Equation 2.15.4
equation2∙15∙4 : {X : Set l} {A B : X → Set l} → ((x : X) → A x × B x) → ((x : X) → A x) × ((x : X) → B x) equation2∙15∙4 f = ((λ x → Σ.fst (f x)) , λ x → Σ.snd (f x))
Theorem 2.15.5
theorem2∙15∙5 : {X : Set l} {A B : X → Set l} → isequiv (equation2∙15∙4 {X = X} {A = A} {B = B}) theorem2∙15∙5 {X = X} {A = A} {B = B} = qinv-to-isequiv (mkQinv g forward backward) where g : ((x : X) → A x) × ((x : X) → B x) → (x : X) → A x × B x g (f , g) x = f x , g x forward : (p : ((x : X) → A x) × ((x : X) → B x)) → equation2∙15∙4 (g p) ≡ p forward p = refl backward : (f : (x : X) → A x × B x) → g (equation2∙15∙4 f) ≡ f backward f = funext λ x → refl where open axiom2∙9∙3
Equation 2.15.6
equation2∙15∙6 : {X : Set} {A : X → Set} {P : (x : X) → A x → Set} → ((x : X) → Σ (A x) (P x)) → Σ ((x : X) → A x) (λ g → (x : X) → P x (g x)) equation2∙15∙6 f = (λ x → fst (f x)) , λ x → snd (f x)
Theorem 2.15.7
theorem2∙15∙7 : {X : Set} {A : X → Set} {P : (x : X) → A x → Set} → isequiv (equation2∙15∙6 {X = X} {A = A} {P = P}) theorem2∙15∙7 {X} {A} {P} = qinv-to-isequiv (mkQinv g forward backward) where open axiom2∙9∙3 g : Σ ((x : X) → A x) (λ g → (x : X) → P x (g x)) → (x : X) → Σ (A x) (P x) g (f1 , f2) x = f1 x , f2 x forward : (equation2∙15∙6 ∘ g) ∼ id forward (f1 , f2) = Σ-≡ (refl , refl) backward : (g ∘ equation2∙15∙6) ∼ id backward f = funext λ x → refl