exercise 2.5

html/book.toml

@@ -3,7 +3,7 @@ authors = ["Michael Zhang"]
 language = "en"
 multilingual = false
 src = "src"
-title = "HoTT Book"
+title = "Research"
 
 [preprocessor.katex]
 macros = "./macros.txt"

html/src/SUMMARY.md

@@ -24,4 +24,5 @@
 
 # Van Doorn Dissertation
 
-- [Preliminaries](./generated/VanDoornDissertation.Preliminaries.md)
+- [Preliminaries](./generated/VanDoornDissertation.Preliminaries.md)
+- [HIT](./generated/VanDoornDissertation.HIT.md)

src/HottBook/Chapter2.lagda.md

@@ -118,11 +118,15 @@ record pointed (l : Level) : Set (lsuc l) where
 
 ### Theorem 2.1.6 (Eckmann-Hilton)
 
-TODO
-
 ```
-Ω² : {l : Level} → pointed l → pointed l
-Ω² p = Ω (Ω p)
+module theorem2∙1∙6 where
+  open pointed
+
+  Ω² : {l : Level} → pointed l → pointed l
+  Ω² p = Ω (Ω p)
+
+  -- compose : {l : Level} → (p : pointed l) → Ω² p
+  -- compose a b = ?
 ```
 
 ## 2.2 Functions are functors
@@ -222,6 +226,24 @@ transportconst {l₁} {l₂} {A} {x} {y} B p b =
   J (λ x y p → transport (λ _ → B) p b ≡ b) (λ x → refl) x y p
 ```
 
+### 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
 
 ```
@@ -333,10 +355,10 @@ lemma2∙4∙3 {A} {B} {f} {g} H {x} {y} p = let
 ### Corollary 2.4.4
 
 ```
--- lemma2∙4∙4 : {A : Set} {f : A → A} {H : f ∼ id}
+-- corollary2∙4∙4 : {A : Set} {f : A → A} {H : f ∼ id}
 --   → (x : A)
 --   → H (f x) ≡ ap f (H x)
--- lemma2∙4∙4 {A} {f} {H} x =
+-- corollary2∙4∙4 {A} {f} {H} x =
 --   let g p = H x in
 --   {!   !}
 ```
@@ -996,4 +1018,4 @@ 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)
-```    
+```     

src/HottBook/Chapter2Exercises.lagda.md

@@ -63,7 +63,11 @@ $A$, simultaneously with the type of boundaries for such paths._
 [6]: https://git.mzhang.io/school/type-theory/issues/6
 
 ```
-
+data n-dimensional-path {A : Set} : (n : ℕ) → Set where
+  z : (x y : A) → x ≡ y → n-dimensional-path zero
+  s : (n : ℕ) → (d : n-dimensional-path {A} n) → n-dimensional-path (suc n)
+-- n-dimensional-path {A} zero = (x y : A) → x ≡ y
+-- n-dimensional-path {A} (suc n) = {!   !}
 ```
 
 ## Exercise 2.5
@@ -73,6 +77,29 @@ Prove that the functions [2.3.6] and [2.3.7] are inverse equivalences.
 [2.3.6]: https://hott.github.io/book/hott-ebook-1357-gbe0b8e2.pdf#equation.2.3.6
 [2.3.7]: https://hott.github.io/book/hott-ebook-1357-gbe0b8e2.pdf#equation.2.3.7
 
+```
+module exercise2∙5 {A B : Set} {x y : A} {p : x ≡ y} {f : A → B} where
+  p1 = transportconst B p (f x)
+
+  forward : (q : f x ≡ f y) → equation2∙3∙7 {p = p} (equation2∙3∙6 {p = p} q) ≡ q
+  forward q = 
+    let 
+      z1 = lemma2∙1∙4.ii1 p1 
+      z = ap (λ r → r ∙ q) z1
+      z2 = lemma2∙1∙4.iv (sym p1) p1 q
+      z3 = sym (lemma2∙1∙4.i2 q)
+    in z2 ∙ z ∙ z3
+
+  backward : (q : transport (λ _ → B) p (f x) ≡ f y) → equation2∙3∙6 {p = p} (equation2∙3∙7 {p = p} q) ≡ q
+  backward q =
+    let
+      z1 = lemma2∙1∙4.ii2 p1
+      z2 = ap (λ r → r ∙ q) z1
+      z3 = lemma2∙1∙4.iv p1 (sym p1) q
+      z4 = sym (lemma2∙1∙4.i2 q)
+    in z3 ∙ z2 ∙ z4
+```
+
 ## Exercise 2.9
 
 Prove that coproducts have the expected universal property,