From 87ab99506cec34e00e06d895fd49ff139544f029 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Fri, 17 May 2024 13:50:46 -0500
Subject: [PATCH] progress

---
 Makefile                       |   7 +-
 html/.gitignore                |   4 +-
 html/book.toml                 |   5 +-
 html/style.css                 |  16 +-
 src/HottBook/Chapter1.lagda.md |   7 +
 src/HottBook/Chapter2.lagda.md | 344 +++++++++++++++++++++++++--------
 src/HottBook/Util.agda         |   3 -
 7 files changed, 294 insertions(+), 92 deletions(-)

diff --git a/Makefile b/Makefile
index 9d857fe..5c4affa 100644
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,12 @@
 GENDIR := html/src/generated
 build-to-html:
 	find src/HottBook \( -name "*.agda" -o -name "*.lagda.md" \) -print0 \
-	  | rust-parallel -0 agda --html --html-dir=$(GENDIR) --html-highlight=auto || true
+	  | rust-parallel -0 agda \
+	  	--html \
+		--html-dir=$(GENDIR) \
+		--allow-unsolved-metas \
+		--html-highlight=auto \
+	  || true
 	fd --no-ignore "html$$" $(GENDIR) -x rm
 
 deploy: build-to-html
diff --git a/html/.gitignore b/html/.gitignore
index 882e309..8ae0f7c 100644
--- a/html/.gitignore
+++ b/html/.gitignore
@@ -1,3 +1,5 @@
 book
 src/generated/*
-!src/generated/.gitkeep
\ No newline at end of file
+!src/generated/.gitkeep
+theme/pagetoc.css
+theme/pagetoc.js
\ No newline at end of file
diff --git a/html/book.toml b/html/book.toml
index 8e59a01..a46ad34 100644
--- a/html/book.toml
+++ b/html/book.toml
@@ -5,5 +5,8 @@ multilingual = false
 src = "src"
 title = "HoTT Book"
 
+[preprocessor.pagetoc]
+
 [output.html]
-additional-css = ["src/generated/Agda.css", "style.css"]
+additional-js = ["theme/pagetoc.js"]
+additional-css = ["src/generated/Agda.css", "style.css", "theme/pagetoc.css"]
diff --git a/html/style.css b/html/style.css
index c66e210..2a60e08 100644
--- a/html/style.css
+++ b/html/style.css
@@ -1,13 +1,11 @@
-
 @font-face {
-    font-family: "PragmataPro Mono Liga";
-    src:
-      url("/fonts/patched/PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2") format("woff2"),
-      url("https://mzhang.io/fonts/patched/PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2")
-        format("woff2");
-  }
-    
+  font-family: "PragmataPro Mono Liga";
+  src:
+    url("/fonts/patched/PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2") format("woff2"),
+    url("https://mzhang.io/fonts/patched/PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2")
+      format("woff2");
+}
 
 pre.Agda  {
-    font-family: "PragmataPro Mono Liga", monospace;
+  font-family: "PragmataPro Mono Liga", monospace;
 }
\ No newline at end of file
diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md
index d631b82..8c14b1f 100644
--- a/src/HottBook/Chapter1.lagda.md
+++ b/src/HottBook/Chapter1.lagda.md
@@ -12,6 +12,11 @@ open import Agda.Primitive
 
 ## 1.4 Dependent function types (Π-types)
 
+```
+id : {l : Level} {A : Set l} → A → A
+id x = x
+```
+
 ## 1.5 Product types
 
 ```
@@ -153,6 +158,8 @@ composite : {A B C : Set}
   → A → C
 composite f g x = g (f x)
 
+-- https://agda.github.io/agda-stdlib/master/Function.Base.html
+infixr 9 _∘_
 _∘_ : {l : Level} {A B C : Set l}
   → (g : B → C)
   → (f : A → B)
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 6399a63..05782c4 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -13,12 +13,16 @@ open import HottBook.Util
 
 ## 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} p = J (λ x y p → y ≡ x) (λ x → refl) x y p
 ```
 
+### Lemma 2.1.2
+
 ```
 trans : {l : Level} {A : Set l} {x y z : A}
   → (x ≡ y)
@@ -32,6 +36,78 @@ trans {l} {A} {x} {y} {z} p q =
 _∙_ = trans
 ```
 
+### Equational Reasoning
+
+```
+module ≡-Reasoning where
+  infix 1 begin_
+  begin_ : {A : Set} {x y : A} → (x ≡ y) → (x ≡ y)
+  begin x = x
+
+  _≡⟨⟩_ : {A : Set} (x {y} : A) → x ≡ y → x ≡ y
+  _ ≡⟨⟩ x≡y = x≡y
+
+  infixr 2 _≡⟨⟩_ step-≡
+  step-≡ : {A : Set} (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 _∎
+  _∎ : {A : Set} (x : A) → (x ≡ x)
+  _ ∎ = refl
+```
+
+### Lemma 2.1.4
+
+```
+record lemma2∙1∙4-statement {A : Set} {x y z w : A}
+    (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) : Set where
+  field
+    i1 : p ≡ p ∙ refl
+    i2 : p ≡ refl ∙ p
+    ii1 : (sym p) ∙ p ≡ refl
+    ii2 : p ∙ (sym p) ≡ refl
+    iii : sym (sym p) ≡ p
+    iv : p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
+
+lemma2∙1∙4 : {A : Set} {x y z w : A}
+  → (p : x ≡ y) 
+  → (q : y ≡ z) 
+  → (r : z ≡ w) 
+  → lemma2∙1∙4-statement p q r
+```
+
+(Proof appears below ap)
+
+### Definition 2.1.7 (pointed type)
+
+This comes first, since it is needed to define Theorem 2.1.6.
+
+```
+record pointed (l : Level) : Set (lsuc l) where
+  eta-equality
+  constructor mkPointed
+  field
+    A : Set l
+    a : A
+```
+
+### Definition 2.1.8 (loop space)
+
+```
+Ω : {l : Level} → pointed l → pointed l
+Ω (mkPointed A a) = mkPointed (a ≡ a) refl
+```
+
+### Theorem 2.1.6 (Eckmann-Hilton)
+
+TODO
+
+```
+Ω² : {l : Level} → pointed l → pointed l
+Ω² p = Ω (Ω p)
+```
+
 ## 2.2 Functions are functors
 
 ### Lemma 2.2.1
@@ -44,6 +120,43 @@ ap : {l : Level} {A B : Set l} {x y : A}
 ap {l} {A} {B} {x} {y} f p = J (λ x y p → f x ≡ f y) (λ x → refl) x y p
 ```
 
+<details>
+  <summary>Proof of Lemma 2.1.4</summary>
+
+```
+
+lemma2∙1∙4 {A} {x} {y} {z} {w} p q r =
+  let
+    i2 : (x y : A) (p : x ≡ y) → p ≡ refl ∙ p
+    i2 x y p = J (λ x y p → p ≡ refl ∙ p) (λ _ → refl) x y p
+  in record 
+  { i1 = J (λ x y p → p ≡ p ∙ refl) (λ _ → refl) x y p
+  ; i2 = i2 x y p
+  ; ii1 = J (λ x y p → (sym p) ∙ p ≡ refl) (λ _ → refl) x y p
+  ; ii2 = J (λ x y p → p ∙ (sym p) ≡ refl) (λ _ → refl) x y p
+  ; iii = J (λ x y p → sym (sym p) ≡ p) (λ _ → refl) x y p
+  ; iv = 
+      let
+        C : (x y : A) → (p : x ≡ y) → Set
+        C x y p = (q : y ≡ z) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
+
+        wtf : (x : A) (q1 : x ≡ z) → (q1 ∙ r) ≡ (refl ∙ (q1 ∙ r))
+        wtf x q1 = i2 x w (q1 ∙ r)
+
+        wtf2 : (x : A) (q1 : x ≡ z) → q1 ≡ (refl ∙ q1)
+        wtf2 x q1 = i2 x z q1
+
+        wtf3 : (x : A) (q1 : x ≡ z) → (q1 ∙ r) ≡ ((refl ∙ q1) ∙ r)
+        wtf3 x q1 = ap (λ x → x ∙ r) (wtf2 x q1)
+
+        c : (x : A) → C x x refl
+        c x q1 = trans (sym (wtf x q1)) (wtf3 x q1)
+      in J C c x y p q
+  }
+```
+
+</details>
+
 ## 2.3 Type families are fibrations
 
 ### Lemma 2.3.1 (Transport)
@@ -118,23 +231,22 @@ lemma2∙3∙8 {l} {A} {B} f {x} {y} p =
 ### Lemma 2.3.9
 
 ```
--- lemma239 : {A : Set} {P : A → Set} {x y z : A}
---   → (p : x ≡ y) → (q : y ≡ z) → (u : P x)
---   → transport P q (transport P p u) ≡ transport P (p ∙ q) u
--- lemma239 {A} {P} p q u =
---   let
---     inner : transport P refl (transport P p u) ≡ transport P p u
---     inner = refl
-
---     ok : p ∙ refl ≡ p
---     ok = J (λ _ r → r ∙ refl ≡ r) p refl
-
---     bruh : transport P (p ∙ refl) u ≡ transport P p u
---     bruh = ap (λ r → transport P r u) ok
---   in
---   J (λ _ what →
---     transport P what (transport P p u) ≡ transport P (p ∙ what) u
---   ) q (inner ∙ sym bruh)
+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 p q u = 
+  let 
+    f2 : (x1 : A) → (q1 : x1 ≡ z) (u1 : P x1) → transport P q1 u1 ≡ transport P (refl ∙ q1) u1
+    f2 x1 q1 u1 =
+      let
+        properties = lemma2∙1∙4 q1 refl refl
+        property = lemma2∙1∙4-statement.i2 properties
+      in
+      ap (λ x → transport P x u1) property
+    f1 = J (λ x1 y1 p1 → (q1 : y1 ≡ z) → (u1 : P x1) → transport P q1 (transport P p1 u1) ≡ transport P (p1 ∙ q1) u1) f2 x y p
+  in f1 q u
 ```
 
 ### Lemma 2.3.10
@@ -186,16 +298,16 @@ Homotopy forms an equivalence relation:
 ∼-refl f x = refl
 
 ∼-sym : {A : Set} {P : A → Set}
-  → (f g : (x : A) → P x)
+  → {f g : (x : A) → P x}
   → f ∼ g → g ∼ f
-∼-sym f g f∼g x = sym (f∼g x)
+∼-sym {f} {g} f∼g x = sym (f∼g x)
 
-∼-trans : {A : Set} {P : A → Set}
-  → (f g h : (x : A) → P 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 f g h f∼g g∼h x = f∼g x ∙ g∼h x
+∼-trans {l} {A} {P} {f} {g} {h} f∼g g∼h x = f∼g x ∙ g∼h x
 ```
 
 ### Lemma 2.4.3
@@ -214,31 +326,55 @@ record qinv {l : Level} {A B : Set l} (f : A → B) : Set l where
   constructor mkQinv
   field
     g : B → A
-    α : f ∘ g ∼ id
-    β : g ∘ f ∼ id
+    α : (f ∘ g) ∼ id
+    β : (g ∘ f) ∼ id
 ```
 
 ### Example 2.4.7
 
 ```
 id-qinv : {l : Level} {A : Set l} → qinv {l} {A} id
-id-qinv = record
-  { g = id
-  ; α = λ _ → refl
-  ; β = λ _ → refl
-  }
+id-qinv = mkQinv id (λ _ → refl) (λ _ → refl)
+```
+
+### Example 2.4.8
+
+```
+
+```
+
+### 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
+    let properties = lemma2∙1∙4 p refl refl in
+    let property = lemma2∙1∙4-statement.ii1 properties in
+    trans wtf (ap (λ x → transport P x py) property)) 
+  (λ px → 
+    let wtf = lemma2∙3∙9 P p (sym p) px in
+    let properties = lemma2∙1∙4 p refl refl in
+    let property = lemma2∙1∙4-statement.ii2 properties in
+    trans wtf (ap (λ x → transport P x px) property)) 
 ```
 
 ### Definition 2.4.10
 
 ```
 record isequiv {l : Level} {A B : Set l} (f : A → B) : Set l where
+  eta-equality
   constructor mkIsEquiv
   field
     g : B → A
-    g-id : f ∘ g ∼ id
+    g-id : (f ∘ g) ∼ id
     h : B → A
-    h-id : h ∘ f ∼ id
+    h-id : (h ∘ f) ∼ id
 ```
 
 ```
@@ -246,12 +382,25 @@ qinv-to-isequiv : {l : Level} {A B : Set l}
   → {f : A → B}
   → qinv f
   → isequiv f
-qinv-to-isequiv q = record
-  { g = qinv.g q
-  ; g-id = qinv.α q
-  ; h = qinv.g q
-  ; h-id = qinv.β q
-  }
+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
@@ -261,6 +410,49 @@ _≃_ : {l : Level} → (A B : Set l) → Set l
 A ≃ B = Σ[ f ∈ (A → B) ] (isequiv f)
 ```
 
+### Lemma 2.4.12
+
+```
+id-equiv : (A : Set) → A ≃ A
+id-equiv A = id , e
+  where
+    e : isequiv id
+    e = mkIsEquiv id (λ _ → refl) id (λ _ → refl)
+
+sym-equiv : {A B : Set} → (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} → (f : A ≃ B) → (g : B ≃ C) → A ≃ C
+trans-equiv {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)
+```
+
 ## 2.7 Σ-types
 
 ### Theorem 2.7.2
@@ -280,10 +472,10 @@ theorem2∙7∙2 {l} {A} {P} (w @ (w1 , w2)) (w' @ (w'1 , w'2)) =
     g : Σ (w1 ≡ w'1) (λ p → transport P p w2 ≡ w'2) → (w ≡ w') 
     g (refl , refl) = refl
 
-    forwards : f ∘ g ∼ id
+    forwards : (f ∘ g) ∼ id
     forwards (refl , refl) = refl
 
-    backwards : g ∘ f ∼ id
+    backwards : (g ∘ f) ∼ id
     backwards refl = refl
 ```
 
@@ -352,44 +544,16 @@ postulate
 ### Lemma 2.10.1
 
 ```
--- idToEquiv : {A B : Set}
---   → (A ≡ B)
---   → A ≃ B
--- idToEquiv {A} {B} p = func , equiv
---   where
---     func : A → B
---     func a = transport id p a
+idtoeqv : {l : Level} {A B : Set l}
+  → (A ≡ B)
+  → (A ≃ B)
+idtoeqv {l} {A} {B} p = J C c A B p
+  where
+    C : (x y : Set l) (p : x ≡ y) → Set l
+    C x y p = x ≃ y
 
---     func-inv : B → A
---     func-inv b = transport id (sym p) b
-
---     p* : A → B
---     p* = transport id p
-
---     wtf3 : A → A
---     wtf3 = J (λ A' B' p' → A → A') (λ A' → {! id  !}) A B p
-
---     wtf3-is-id : wtf3 ∼ id
---     wtf3-is-id x = {!  !}
-
---     wtf3-qinv : qinv wtf3
---     wtf3-qinv = record
---       { g = wtf3
---       ; α = λ x → {!   !}
---       ; β = λ x → {!   !}
---       }
-
---     -- homotopy : (func ∘ func-inv) ∼ id
---     -- homotopy x = 
---     --   let
---     --   in {!    !}
-
---     equiv = record
---       { g = func-inv
---       ; g-id = {!   !}
---       ; h = func-inv
---       ; h-id = {!   !}
---       }
+    c : (x : Set l) → C x x refl
+    c x = id , qinv-to-isequiv id-qinv
 ```
 
 ### Axiom 2.10.3 (Univalence)
@@ -399,6 +563,32 @@ postulate
   ua : {A B : Set} (eqv : A ≃ B) → (A ≡ B)
 ```
 
+### 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 , mkIsEquiv g g-id h h-id) a a' = ap f , qinv-to-isequiv eqv
+  where
+    inv : f a ≡ f a' → a ≡ a'
+    inv p = trans {!   !} (trans (ap g p) {!   !})
+    eqv = mkQinv {! !} {!   !} {!   !}
+```
+
 ## 2.13 Natural numbers
 
 ```
@@ -496,4 +686,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)
-``` 
\ No newline at end of file
+```   
\ No newline at end of file
diff --git a/src/HottBook/Util.agda b/src/HottBook/Util.agda
index 2d2c052..fa7ab3e 100644
--- a/src/HottBook/Util.agda
+++ b/src/HottBook/Util.agda
@@ -1,6 +1,3 @@
 module HottBook.Util where
 
 open import Agda.Primitive
-
-id : {l : Level} {A : Set l} → A → A
-id x = x
\ No newline at end of file