From 71b5471d1455352d52f674b6f2a7243a25df6621 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 20 May 2024 16:52:39 -0500
Subject: [PATCH] progress

---
 html/style.css                 |  2 +-
 src/HottBook/Chapter1.lagda.md |  9 ++++-
 src/HottBook/Chapter1Util.agda |  7 ++++
 src/HottBook/Chapter2.lagda.md | 25 +++++++++---
 src/HottBook/Chapter3.lagda.md | 73 ++++++++++++++++++++++++++--------
 src/HottBook/Chapter6.lagda.md |  4 +-
 src/HottBook/Chapter8.lagda.md |  7 ++++
 7 files changed, 101 insertions(+), 26 deletions(-)

diff --git a/html/style.css b/html/style.css
index 2a60e08..922465e 100644
--- a/html/style.css
+++ b/html/style.css
@@ -6,6 +6,6 @@
       format("woff2");
 }
 
-pre.Agda  {
+pre.Agda, pre code {
   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 2969f37..16b7864 100644
--- a/src/HottBook/Chapter1.lagda.md
+++ b/src/HottBook/Chapter1.lagda.md
@@ -100,6 +100,12 @@ data 𝟚 : Set where
   false : 𝟚
 ```
 
+```
+neg : 𝟚 → 𝟚
+neg true = false
+neg false = true
+```
+
 ## 1.9 The natural numbers
 
 ```
@@ -116,6 +122,7 @@ rec-ℕ C z s (suc n) = s n (rec-ℕ C z s n)
 ## 1.11 Propositions as types
 
 ```
+infix 3 ¬_
 ¬_ : {l : Level} (A : Set l) → Set l
 ¬ A = A → ⊥
 ```
@@ -161,7 +168,7 @@ 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}
+_∘_ : {l1 l2 l3 : Level} {A : Set l1} {B : Set l2} {C : Set l3}
   → (g : B → C)
   → (f : A → B)
   → A → C
diff --git a/src/HottBook/Chapter1Util.agda b/src/HottBook/Chapter1Util.agda
index 9c9dfc0..d6dbb9c 100644
--- a/src/HottBook/Chapter1Util.agda
+++ b/src/HottBook/Chapter1Util.agda
@@ -10,3 +10,10 @@ open import HottBook.Util
   → Σ (a₁ ≡ a₂) (λ p → transport B p b₁ ≡ b₂)
   → p₁ ≡ p₂
 Σ-≡ {l₁} {l₂} {A} {B} {p₁ @ (a₁ , b₁)} {p₂ @ (a₂ , b₂)} (refl , refl) = refl
+
+neg-homotopy : (neg ∘ neg) ∼ id
+neg-homotopy true = refl
+neg-homotopy false = refl
+
+neg-equiv : 𝟚 ≃ 𝟚
+neg-equiv = neg , qinv-to-isequiv (mkQinv neg neg-homotopy neg-homotopy)
\ No newline at end of file
diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index edd8c0c..359dd72 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -385,7 +385,7 @@ transport-qinv P p = mkQinv (transport P (sym p))
 ### Definition 2.4.10
 
 ```
-record isequiv {l : Level} {A B : Set l} (f : A → B) : Set l where
+record isequiv {l1 l2 : Level} {A : Set l1} {B : Set l2} (f : A → B) : Set (l1 ⊔ l2) where
   eta-equality
   constructor mkIsEquiv
   field
@@ -424,7 +424,7 @@ isequiv-to-qinv {l} {A} {B} {f} (mkIsEquiv g g-id h h-id) =
 ### Definition 2.4.11
 
 ```
-_≃_ : {l : Level} → (A B : Set l) → Set l
+_≃_ : {l1 l2 : Level} → (A : Set l1) (B : Set l2) → Set (l1 ⊔ l2)
 A ≃ B = Σ[ f ∈ (A → B) ] (isequiv f)
 ```
 
@@ -637,11 +637,11 @@ postulate
 
 ```
 happly : {A B : Set}
-  → (f g : A → B)
-  → {x : A} 
+  → {f g : A → B}
   → (p : f ≡ g)
+  → (x : A)
   → f x ≡ g x
-happly {A} {B} f g {x} p = ap (λ h → h x) p
+happly {A} {B} {f} {g} p x = ap (λ h → h x) p
 ```
 
 ### Axiom 2.9.3 (Function extensionality)
@@ -654,6 +654,19 @@ postulate
     → f ≡ g
 ```
 
+### 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 p =
+  J (λ x3 y3 p1 → (f1 : A x3 → B x3) → (transport (λ x → A x → B x) p1 f1 ≡ λ x → transport B p1 (f1 (transport A (sym p1) x))))
+  (λ x3 f1 → refl) x1 x2 p f
+```
+
 ### Lemma 2.9.6
 
 ```
@@ -697,7 +710,7 @@ idtoeqv {l} {A} {B} p = J C c A B p
 ```
 module axiom2∙10∙3 where
   postulate
-    -- ua-eqv : {l : Level} {A B : Set l} → (A ≃ B) ≃ (A ≡ B)
+    -- ua-eqv : {l1 l2 : Level} {A : Set l1} {B : Set l2} → (A ≃ B) ≃ (A ≡ B)
 
     ua : {l : Level} {A B : Set l} → (A ≃ B) → (A ≡ B)
 
diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index 8979f1d..7292f4b 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -46,25 +46,14 @@ isSet A = (x y : A) → (p q : x ≡ y) → p ≡ q
 
 ```
 example3∙1∙9 : ¬ (isSet Set)
-example3∙1∙9 p = {!   !}
+example3∙1∙9 p = remark2∙12∙6 lol
   where
     open axiom2∙10∙3
 
-    f : 𝟚 → 𝟚
-    f true = false
-    f false = true
-
-    f-homotopy : (f ∘ f) ∼ id
-    f-homotopy true = refl
-    f-homotopy false = refl
-
-    f-equiv : 𝟚 ≃ 𝟚
-    f-equiv = f , qinv-to-isequiv (mkQinv f f-homotopy f-homotopy)
-
     f-path : 𝟚 ≡ 𝟚
-    f-path = ua f-equiv
+    f-path = ua neg-equiv
 
-    bogus : f ≡ id
+    bogus : id ≡ neg
     bogus =
       let
         helper : f-path ≡ refl
@@ -75,15 +64,67 @@ example3∙1∙9 p = {!   !}
         wtf : idtoeqv f-path ≡ idtoeqv refl
         wtf = ap idtoeqv helper
       in {!   !}
+
+    lol : true ≡ false
+    lol = ap (λ f → f true) bogus
 ```
 
 ## 3.2 Propositions as types?
 
 ### Theorem 3.2.2
 
+TODO: Study this more
+
 ```
-theorem3∙2∙2 : ((A : Set) → (¬ (¬ A) → A)) → ⊥
-theorem3∙2∙2 p = {!   !}
+theorem3∙2∙2 : ((A : Set) → ¬ ¬ A → A) → ⊥
+theorem3∙2∙2 f = let wtf = f 𝟚 in {!   !}
+  where
+    open axiom2∙10∙3
+
+    p : 𝟚 ≡ 𝟚
+    p = ua neg-equiv
+
+    wtf : ¬ ¬ 𝟚 → 𝟚
+    wtf = f 𝟚
+
+    wtf2 : transport (λ A → ¬ ¬ A → A) p (f 𝟚) ≡ f 𝟚
+    wtf2 = apd f p
+
+    wtf3 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ f 𝟚 u
+    wtf3 u = happly wtf2 u
+
+    wtf4 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A → A) p (f 𝟚) u ≡ transport (λ A → A) p (f 𝟚 (transport (λ A → ¬ ¬ A) (sym p) u))
+    wtf4 u = 
+      let
+        wtf5 : 
+          let A = λ A → ¬ ¬ A in
+          let B = id in
+          transport (λ x → A x → B x) p (f 𝟚) ≡ λ x → transport B p (f 𝟚 (transport A (sym p) x))
+        wtf5 = equation2∙9∙4 (f 𝟚) p
+      in
+      happly wtf5 u
+
+    wtf6 : (u v : ¬ ¬ 𝟚) → u ≡ v
+    wtf6 u v = funext (λ x → rec-⊥ (u x))
+
+    wtf7 : (u : ¬ ¬ 𝟚) → transport (λ A → ¬ ¬ A) (sym p) u ≡ u
+    wtf7 u = {!   !}
+
+    wtf8 : (u : ¬ ¬ 𝟚) → transport (λ A → A) p (f 𝟚 u) ≡ f 𝟚 u
+    wtf8 u = {!  sym (wtf3 u) !} ∙ sym (wtf4 u) ∙ wtf3 u
+
+    wtf9 : (u : ¬ ¬ 𝟚) → neg (f 𝟚 u) ≡ f 𝟚 u
+    wtf9 = {!   !}
+
+    wtf10 : (x : 𝟚) → ¬ (neg x ≡ x)
+    wtf10 true p = remark2∙12∙6 (sym p)
+    wtf10 false p = remark2∙12∙6 p
+
+    wtf11 : (u : ¬ ¬ 𝟚) → ¬ (neg (f 𝟚 u) ≡ (f 𝟚 u))
+    wtf11 u = wtf10 (f 𝟚 u)
+
+    wtf12 : (u : ¬ ¬ 𝟚) → ⊥
+    wtf12 u = wtf11 u (wtf9 u)
 ```
 
 ### Corollary 3.2.7
diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md
index 8211f3f..3a0e4e3 100644
--- a/src/HottBook/Chapter6.lagda.md
+++ b/src/HottBook/Chapter6.lagda.md
@@ -47,8 +47,8 @@ lemma6∙2∙5 {A} a p circ = S¹-elim P p-base p-loop circ
 
     p-loop : transport P loop a ≡ a
     p-loop =
-      let wtf = lemma2∙3∙8 loop in
-      {!   !}
+      let wtf = lemma2∙3∙8 (λ x → {!   !}) loop in
+      {!    !}
 ```
 
 ## 6.3 The interval
diff --git a/src/HottBook/Chapter8.lagda.md b/src/HottBook/Chapter8.lagda.md
index b951e37..0e7f22c 100644
--- a/src/HottBook/Chapter8.lagda.md
+++ b/src/HottBook/Chapter8.lagda.md
@@ -7,6 +7,13 @@ open import HottBook.Chapter2
 open import HottBook.Chapter6
 ```
 
+### Definition 8.0.1
+
+```
+π : (n : ℕ) → (A : Set) → (a : A) → Set
+
+```
+
 ## 8.1 π₁(S¹)
 
 ### Definition 8.1.1