From 33c42508ad3386a1b43c00aa3d9c2c4e8f2350eb Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 29 Apr 2024 14:19:48 -0400
Subject: [PATCH] more progress

---
 src/HottBook/Chapter1.lagda.md          |   6 +-
 src/HottBook/Chapter2Exercises.lagda.md | 118 ++++++++----------------
 2 files changed, 45 insertions(+), 79 deletions(-)

diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md
index 612e516..dc4c4e6 100644
--- a/src/HottBook/Chapter1.lagda.md
+++ b/src/HottBook/Chapter1.lagda.md
@@ -114,7 +114,11 @@ composite : {A B C : Set}
   → A → C
 composite f g x = g (f x)
 
-syntax composite f g = g ∘ f
+_∘_ : {A B C : Set}
+  → (g : B → C)
+  → (f : A → B)
+  → A → C
+_∘_ g f x = g (f x)
 
 composite-assoc : {A B C D : Set}
   → (f : A → B)
diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md
index 67659e6..079aa64 100644
--- a/src/HottBook/Chapter2Exercises.lagda.md
+++ b/src/HottBook/Chapter2Exercises.lagda.md
@@ -51,89 +51,51 @@ main proof:
 
 ```
 exercise2∙13 : (𝟚 ≃ 𝟚) ≃ 𝟚
-exercise2∙13 = aux1 , equiv1
+exercise2∙13 = f , equiv
   where
-    aux1 : 𝟚 ≃ 𝟚 → 𝟚
-    aux1 (fst , snd) = fst true
-
     neg : 𝟚 → 𝟚
     neg true = false
     neg false = true
 
-    neg-homotopy : (neg ∘ neg) ∼ id
-    neg-homotopy true = refl
-    neg-homotopy false = refl
+    f : 𝟚 ≃ 𝟚 → 𝟚
+    f (fst , snd) = fst true
 
-    open Σ
-    open isequiv
-
-    rev : 𝟚 → (𝟚 ≃ 𝟚)
-    fst (rev true) = id
-    g (snd (rev true)) = id
-    g-id (snd (rev true)) x = refl
-    h (snd (rev true)) = id
-    h-id (snd (rev true)) x = refl
-    fst (rev false) = neg
-    g (snd (rev false)) = neg
-    g-id (snd (rev false)) = neg-homotopy
-    h (snd (rev false)) = neg
-    h-id (snd (rev false)) = neg-homotopy
-
-    equiv1 : isequiv aux1
-    g equiv1 = rev
-    g-id equiv1 true = refl
-    g-id equiv1 false = refl
-    h equiv1 = rev
-    h-id equiv1 e@(f , f-equiv @ (mkIsEquiv g g-id h h-id)) =
-      -- proving that given any equivalence e, that:
-      --   ((aux1 ∘ rev) e ≡ id e)
-      --   (rev (aux1 e) ≡ e)
-      --   (rev (e.fst true) ≡ e)
-      -- since e is a pair, decompose it using Σ-≡ and prove separately that:
-      -- - fst (rev (e.fst true)) ≡ e.fst
-      --   - left side is a function and right side is a function too
-      --   - use function extensionality to show they behave the same
-      --   - somehow use the fact that e.snd.g-id exists
-      -- - snd (rev (e.fst true)) ≡ e.snd
-        -- test1 : (x : 𝟚) → fst (aux1 x) ≡ f x
-        -- test1 x with x , f true
-        -- test1 _ | true , true = {!  !}
-        -- test1 _ | true , false = {!  !}
-        -- test1 _ | false , y = {!   !}
-
-        -- equiv-funcs : (x : 𝟚) → aux1 x ≡ f x
-
-        -- -- if f mapped everything to the same value, then the inverse couldn't exist
-        -- -- how to state this as a proof?
-
-        -- asdf : (x : 𝟚) → neg (f x) ≡ f (neg x)
-        -- -- known that (f ∘ g) x ≡ x
-        -- -- g (f x) ≡ x
-        -- -- g (f true) ≡ true
-        -- -- maybe a proof by contradiction? suppose f true ≡ f false. why doesn't this work if f ∘ g ∼ id?
-        -- -- how to work backwards from the f ∘ g ∼ id? since we have a value `g-id` of that
-        -- asdf true = {!   !}
-        -- asdf false = {!   !}
-
-        -- ft = f true
-        -- ff = f false
-
-        -- div : ft ≢ ff
-        -- div p =
-        --   let
-        --     id𝟚 : 𝟚 → 𝟚
-        --     id𝟚 = id
-
-        --     wtf : ft ≡ ff
-        --     wtf = p
-
-        --     wtf2 : g ft ≡ g ff
-        --     wtf2 = ap g wtf
-
-        --   in {!   !}
-        -- in Σ-≡ (funext test1 , {!   !})
-      {!   !}
+    g : 𝟚 → 𝟚 ≃ 𝟚
+    g true = id , mkIsEquiv id (λ _ → refl) id (λ _ → refl)
+    g false = neg , mkIsEquiv neg neg-id neg neg-id
       where
-        test1 : (x : 𝟚 ≃ 𝟚) → aux1 x ≡ {!   !}
-        test1 (x , y) = {!  !}
+        neg-id : (neg ∘ neg) ∼ id
+        neg-id true = refl
+        neg-id false = refl
+
+    f∘g∼id : f ∘ g ∼ id
+    f∘g∼id true = refl
+    f∘g∼id false = refl
+
+    g∘f∼id : g ∘ f ∼ id
+    g∘f∼id e' @ (f' , ie' @ (mkIsEquiv g' g-id h' h-id)) = {!   !}
+      where
+        f-codomain-is-2 : f' true ≢ f' false
+        f-codomain-is-2 p = {!   !}
+
+        f-true-is-true-to-id : f' true ≡ true → f' ≡ id
+        f-true-is-true-to-id p = funext prf
+          where
+            prf : (x : 𝟚) → f' x ≡ id x
+            prf true = p
+            prf false with f' false
+            prf false | true = {!   !}
+            prf false | false = refl
+
+        equivPrf' : (x : 𝟚) → Σ.fst (g (f' true)) x ≡ f' x
+        equivPrf' x = {!   !}
+
+        equivPrf : Σ.fst (g (f' true)) ≡ f'
+        equivPrf = funext equivPrf'
+
+        attempt : (g ∘ f) e' ≡ id e'
+        attempt = posEqLemma ((g ∘ f) e') (id e') equivPrf
+
+    equiv : isequiv f
+    equiv = mkIsEquiv g f∘g∼id g g∘f∼id
 ```