From c8ddc593bc42f733f2a1d4389504ac45d0b8e823 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 25 Jul 2024 07:31:02 -0500
Subject: [PATCH] nya

---
 html/src/SUMMARY.md            |  2 ++
 src/HottBook/Chapter2.lagda.md | 45 ++++++++++++++++++++++++++++------
 src/HottBook/Chapter6.lagda.md |  1 -
 3 files changed, 40 insertions(+), 8 deletions(-)

diff --git a/html/src/SUMMARY.md b/html/src/SUMMARY.md
index 3d38058..d817a58 100644
--- a/html/src/SUMMARY.md
+++ b/html/src/SUMMARY.md
@@ -10,6 +10,8 @@
 - [Chapter 4](./generated/HottBook.Chapter4.md)
 - [Chapter 5](./generated/HottBook.Chapter5.md)
 - [Chapter 6](./generated/HottBook.Chapter6.md)
+- [Chapter 7](./generated/HottBook.Chapter7.md)
+- [Chapter 8](./generated/HottBook.Chapter8.md)
 
 # HoTT Book (Cubical formulation)
 
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index bff06de..cb7a02d 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -96,19 +96,22 @@ pointed l = Σ (Set l) (λ A → A)
 ### Definition 2.1.8 (loop space)
 
 ```
-Ω : {l : Level} → pointed l → pointed l
-Ω (A , a) = (a ≡ a) , refl
+Ω : {l : Level} → pointed l → Set l
+Ω (A , a) = a ≡ a
 ```
 
 ### Theorem 2.1.6 (Eckmann-Hilton)
 
 ```
 module theorem2∙1∙6 where
-  Ω² : {l : Level} → pointed l → pointed l
-  Ω² p = Ω (Ω p)
+  Ω² : {l : Level} → pointed l → Set l
+  Ω² p = Ω (Ω p , refl)
 
-  -- compose : {l : Level} {p : pointed {l}} → (Ω² p) × (Ω² p) → Ω² p
-  -- compose a b = ?
+  compose : {l : Level} {p : pointed l} → (Ω² p) × (Ω² p) → Ω² p
+  compose (a , b) = a ∙ b
+
+  -- commute : {l : Level} {p : pointed l} → (α β : Ω² p) → α ∙ β ≡ β ∙ α
+  -- commute {l} {p @ (A , a₀)} α β = {!  !}
 ```
 
 ## 2.2 Functions are functors
@@ -312,6 +315,7 @@ lemma2∙4∙3 {A} {B} {f} {g} H {x} {y} refl =
 --   → 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 
 --   {!   !}
 ```
 
@@ -1043,4 +1047,31 @@ theorem2∙15∙5 {X = X} {A = A} {B = B} = qinv-to-isequiv (mkQinv g forward ba
     backward : (f : (x : X) → A x × B x) → g (equation2∙15∙4 f) ≡ f
     backward f = funext λ x → refl
       where open axiom2∙9∙3
-```   
\ No newline at end of file
+```    
+
+### 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
+```
\ No newline at end of file
diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md
index 1a1ab29..2952b22 100644
--- a/src/HottBook/Chapter6.lagda.md
+++ b/src/HottBook/Chapter6.lagda.md
@@ -357,7 +357,6 @@ lemma6∙5∙1 = f , qinv-to-isequiv (mkQinv g forward backward)
 
         goal2 : (y : 𝟚) → {!   !} ∙ refl ∙ {!   !} ≡ merid true
         goal y = {!   !}
-
 ```
 
 ### Definition 6.5.2