From 044e7382ee64989d827034075516cf6ef0fca09b Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Wed, 8 May 2024 18:28:14 -0500
Subject: [PATCH] proved 2.13

---
 src/HottBook/Chapter2Exercises.lagda.md | 90 ++++++++++++++++++-------
 1 file changed, 64 insertions(+), 26 deletions(-)

diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md
index 7bc4e42..bcc8969 100644
--- a/src/HottBook/Chapter2Exercises.lagda.md
+++ b/src/HottBook/Chapter2Exercises.lagda.md
@@ -44,11 +44,15 @@ postulate
     → (Σ.fst e1 ≡ Σ.fst e2)
     → e1 ≡ e2
 
-eqLemma : {A B : Set}
-  → (e1 e2 : A ≃ B)
-  → (Σ.fst e1 ≡ Σ.fst e2)
-  → e1 ≡ e2
-eqLemma {A} {B} e1 e2 p = {!   !}
+
+-- What the hell
+-- https://agda.readthedocs.io/en/v2.6.1/language/with-abstraction.html#the-inspect-idiom
+module Wtf {a b} {A : Set a} {B : A → Set b} where
+  data Graph (f : ∀ x → B x) (x : A) (y : B x) : Set b where
+    ingraph : f x ≡ y → Graph f x y
+  inspect : (f : ∀ x → B x) (x : A) → Graph f x (f x)
+  inspect _ _ = ingraph refl
+open Wtf
 ```
 
 main proof:
@@ -64,13 +68,19 @@ exercise2∙13 = f , equiv
     f : 𝟚 ≃ 𝟚 → 𝟚
     f (fst , snd) = fst true
 
+    id-equiv : isequiv id
+    id-equiv = mkIsEquiv id (λ _ → refl) id (λ _ → refl)
+
+    neg-id : (neg ∘ neg) ∼ id
+    neg-id true = refl
+    neg-id false = refl
+
+    neg-equiv : isequiv neg
+    neg-equiv = mkIsEquiv neg neg-id neg neg-id
+
     g : 𝟚 → 𝟚 ≃ 𝟚
-    g true = id , mkIsEquiv id (λ _ → refl) id (λ _ → refl)
-    g false = neg , mkIsEquiv neg neg-id neg neg-id
-      where
-        neg-id : (neg ∘ neg) ∼ id
-        neg-id true = refl
-        neg-id false = refl
+    g true = id , id-equiv
+    g false = neg , neg-equiv
 
     f∘g∼id : f ∘ g ∼ id
     f∘g∼id true = refl
@@ -79,26 +89,54 @@ exercise2∙13 = f , equiv
     g∘f∼id : g ∘ f ∼ id
     g∘f∼id e' @ (f' , ie' @ (mkIsEquiv g' g-id h' h-id)) = attempt
       where
+        Bmap : 𝟚 → Set
+        Bmap true = 𝟙
+        Bmap false = ⊥
+
+        true≢false : true ≢ false
+        true≢false p =
+          let genBot = transport Bmap p in
+          genBot tt
+
         f-codomain-is-2 : f' true ≢ f' false
-        f-codomain-is-2 p = {!   !}
+        f-codomain-is-2 p =
+          let p1 = ap h' p in
+          let p2 = trans p1 (h-id false) in
+          let p3 = trans (sym (h-id true)) p2 in
+          true≢false p3
 
-        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
+        ⊥-elim : {A : Set} → ⊥ → A
+        ⊥-elim ()
 
-        equivPrf' : (x : 𝟚) → Σ.fst (g (f' true)) x ≡ f' x
-        equivPrf' x = {!   !}
+        opposite-prop : {a b : 𝟚} → (p : f' a ≡ b) → f' (neg a) ≡ neg b
+        opposite-prop {a} {b} p with f' (neg a) | inspect f' (neg a)
+        opposite-prop {true} {true} p | true | ingraph q = ⊥-elim (f-codomain-is-2 (trans p (sym q)))
+        opposite-prop {true} {true} p | false | _ = refl
+        opposite-prop {true} {false} p | true | _ = refl
+        opposite-prop {true} {false} p | false | ingraph q = ⊥-elim (f-codomain-is-2 (trans p (sym q)))
+        opposite-prop {false} {true} p | true | ingraph q = ⊥-elim (f-codomain-is-2 (trans q (sym p)))
+        opposite-prop {false} {true} p | false | ingraph q = refl
+        opposite-prop {false} {false} p | true | ingraph q = refl
+        opposite-prop {false} {false} p | false | ingraph q = ⊥-elim (f-codomain-is-2 (trans q (sym p)))
 
-        equivPrf : Σ.fst (g (f' true)) ≡ f'
-        equivPrf = funext equivPrf'
+        f-is-id' : (f' true ≡ true) → (b : 𝟚) → f' b ≡ id b
+        f-is-id' p true = p
+        f-is-id' p false = opposite-prop p
 
-        attempt : (g ∘ f) e' ≡ id e'
-        attempt = posEqLemma ((g ∘ f) e') (id e') equivPrf
+        f-is-id : (f' true ≡ true) → f' ≡ id
+        f-is-id p = funext (f-is-id' p)
+
+        f-is-neg' : (f' true ≡ false) → (b : 𝟚) → f' b ≡ neg b
+        f-is-neg' p true = p
+        f-is-neg' p false = opposite-prop p
+
+        f-is-neg : (f' true ≡ false) → f' ≡ neg
+        f-is-neg p = funext (f-is-neg' p)
+
+        attempt : g (f' true) ≡ e'
+        attempt with (f' true) | inspect f' true
+        attempt | true | ingraph p = posEqLemma (id , id-equiv) e' (sym (f-is-id p))
+        attempt | false | ingraph p = posEqLemma (neg , neg-equiv) e' (sym (f-is-neg p))
 
     equiv : isequiv f
     equiv = mkIsEquiv g f∘g∼id g g∘f∼id