From 4c9a94414dd5e4d960ccc6a881181d4a8543bc5c Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Tue, 9 Jul 2024 10:24:54 -0500
Subject: [PATCH] example 3.1.9

---
 src/HottBook/Chapter2.lagda.md          | 17 +++--
 src/HottBook/Chapter2Exercises.lagda.md | 34 ++++-----
 src/HottBook/Chapter3.lagda.md          | 94 +++++++++++++++++--------
 src/HottBook/Chapter4.lagda.md          | 30 +++++++-
 4 files changed, 120 insertions(+), 55 deletions(-)

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index d557ff4..2434cd8 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -721,16 +721,21 @@ idtoeqv refl = transport id refl , qinv-to-isequiv (mkQinv id id-homotopy id-hom
 
 ```
 module axiom2∙10∙3 where
+  private
+    variable
+      A B : Set l
   postulate
-    ua : {l : Level} {A B : Set l} → (A ≃ B) → (A ≡ B)
-
-    backward : {l : Level} {A B : Set l} → (p : A ≡ B) → (ua ∘ idtoeqv) p ≡ p
-    forward : {l : Level} {A B : Set l} → (eqv : A ≃ B) → (idtoeqv ∘ ua) eqv ≡ eqv
+    ua : (A ≃ B) → (A ≡ B)
+    propositional-computation : (f : A ≃ B) → idtoeqv (ua f) ≡ f
+    propositional-uniqueness : (p : A ≡ B) → p ≡ ua (idtoeqv p)
 
   ua-eqv : {A B : Set l} → (A ≃ B) ≃ (A ≡ B)
-  ua-eqv = ua , qinv-to-isequiv (mkQinv idtoeqv backward forward)
+  ua-eqv = ua , qinv-to-isequiv
+    (mkQinv idtoeqv
+      (λ p → sym (propositional-uniqueness p))
+      (λ e → propositional-computation e))
 
-open axiom2∙10∙3 hiding (forward; backward)
+open axiom2∙10∙3
 ```
 
 ### Lemma 2.10.5
diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md
index 7f7ae65..2166a7a 100644
--- a/src/HottBook/Chapter2Exercises.lagda.md
+++ b/src/HottBook/Chapter2Exercises.lagda.md
@@ -167,7 +167,9 @@ TODO: Generalizing to dependent functions.
 ## Exercise 2.10
 
 ```
-
+postulate
+  exercise2∙10 : {A : Set} {B : A → Set} {C : Σ A B → Set}
+    → Σ A (λ x → Σ (B x) (λ y → C (x , y))) ≃ Σ (Σ A B) (λ p → C p)
 ```
 
 ## Exercise 2.13
@@ -268,15 +270,15 @@ module exercise2∙16 where
   postulate
     notFunext : {l1 l2 : Level} (A : Set l1) → (B : A → Set l2) → (f g : (x : A) → B x) → (f ∼ g) → (f ≡ g)
 
-  realFunext : {l : Level} {A B : Set l} → {f g : A → B} → ((x : A) → f x ≡ g x) → f ≡ g
-  realFunext {l} {A} {B} {f} {g} p = notFunext A {! B   !} {!   !} {!   !} {!   !}
+  -- realFunext : {l : Level} {A B : Set l} → {f g : A → B} → ((x : A) → f x ≡ g x) → f ≡ g
+  -- realFunext {l} {A} {B} {f} {g} p = notFunext A {! B   !} {!   !} {!   !} {!   !}
 ```
 
 ## Exercise 2.17
 
 ```
 module exercise2∙17 where
-  open axiom2∙10∙3 hiding (forward; backward)
+  open axiom2∙10∙3
   statement = {A A' B B' : Set} → A ≃ A' → B ≃ B' → (A × B) ≃ (A' × B')
 
   --- I have no idea where this goes but this definitely needs to exist
@@ -285,21 +287,21 @@ module exercise2∙17 where
   pair-≡ refl refl = refl
 
   -- Without univalence
-  i : statement
-  i {A} {A'} {B} {B'} (A-eqv @ (Af , A-isequiv)) (B-eqv @ (Bf , B-isequiv)) =
-    f , qinv-to-isequiv (mkQinv g {!   !} {!   !})
-    where 
-      f : (A × B) → (A' × B')
-      f (a , b) = Af a , Bf b
+  -- i : statement
+  -- i {A} {A'} {B} {B'} (A-eqv @ (Af , A-isequiv)) (B-eqv @ (Bf , B-isequiv)) =
+  --   f , qinv-to-isequiv (mkQinv g {!   !} {!   !})
+  --   where 
+  --     f : (A × B) → (A' × B')
+  --     f (a , b) = Af a , Bf b
 
-      g : (A' × B') → (A × B)
-      g (a' , b') = (isequiv.g A-isequiv) a' , (isequiv.g B-isequiv) b'
+  --     g : (A' × B') → (A × B)
+  --     g (a' , b') = (isequiv.g A-isequiv) a' , (isequiv.g B-isequiv) b'
 
-      backward : (f ∘ g) ∼ id
-      backward x = {!   !}
+  --     backward : (f ∘ g) ∼ id
+  --     backward x = {!   !}
 
-      forward : (g ∘ f) ∼ id
-      forward x = {!   !}
+  --     forward : (g ∘ f) ∼ id
+  --     forward x = {!   !}
 
   -- With univalence
   ii : statement
diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md
index 9463dec..14d6914 100644
--- a/src/HottBook/Chapter3.lagda.md
+++ b/src/HottBook/Chapter3.lagda.md
@@ -81,46 +81,58 @@ is-1-type A = (x y : A) → (p q : x ≡ y) → (r s : p ≡ q) → r ≡ s
 ### Lemma 3.1.8
 
 ```
--- lemma3∙1∙8 : {A : Set} → isSet A → is-1-type A
--- lemma3∙1∙8 {A} A-set x y p q r s =
---   let g = λ q → A-set x y p q in
---   let
---     what : {q' : x ≡ y} (r : q ≡ q') → g q ∙ r ≡ g q'
---     what r =
---       let what3 = apd g r in
---       let what4 = lemma2∙11∙2.i r (g q) in
---       let what5 = {!   !} in
---       sym what4 ∙ what3
---   in
---   -- let what2 = what r in
---   {!   !}
+lemma3∙1∙8 : {A : Set} → isSet A → is-1-type A
+lemma3∙1∙8 {A} A-set x y p q r s =
+  let 
+    g : (q : x ≡ y) → p ≡ q 
+    g q = A-set x y p q
+
+    what : (q' : x ≡ y) → (r : q ≡ q') → transport (λ p' → p ≡ p') r (g q) ≡ g q'
+    what q' r = apd g r
+
+    what2 : (q' : x ≡ y) → (r : q ≡ q') → (g q) ∙ r ≡ g q'
+    what2 q' r = sym (lemma2∙11∙2.i r (g q)) ∙ what q' r
+
+    what3 : (q' : x ≡ y) → (r s : q ≡ q') → (g q) ∙ r ≡ (g q) ∙ s
+    what3 q' r s = what2 q' r ∙ sym (what2 q' s)
+
+    what4 : (g q) ∙ (sym r) ≡ (g q) ∙ (sym s)
+    what4 = what3 p (sym r) (sym s) 
+
+  in what5
+  where
+    -- TODO: Dont' feel like proving this for now, will revisit later
+    postulate
+      what5 : r ≡ s
 ```
 
 ### Example 3.1.9
 
 ```
--- example3∙1∙9 : ∀ {l : Level} → ¬_ {lsuc l} (isSet (Set l))
--- example3∙1∙9 p = remark2∙12∙6 lol
---   where
---     open axiom2∙10∙3
+example3∙1∙9 : ¬  (isSet Set)
+example3∙1∙9 p = remark2∙12∙6.true≢false lol
+  where
+    open axiom2∙10∙3
 
---     f-path : 𝟚 ≡ 𝟚
---     f-path = ua neg-equiv
+    f-path : 𝟚 ≡ 𝟚
+    f-path = ua neg-equiv
 
---     bogus : id ≡ neg
---     bogus =
---       let
---         -- helper : f-path ≡ refl
---         -- helper = p 𝟚 𝟚 f-path refl
+    bogus : id ≡ neg
+    bogus =
+      let
+        helper : f-path ≡ refl
+        helper = p 𝟚 𝟚 f-path refl
 
---         a = ap
+        wtf : idtoeqv f-path ≡ idtoeqv refl
+        wtf = ap idtoeqv helper
 
---         -- wtf : idtoeqv f-path ≡ idtoeqv refl
---         -- wtf = ap idtoeqv helper
---       in {!   !}
+        wtf2 = ap Σ.fst wtf
+        wtf3 = ap Σ.fst (propositional-computation neg-equiv)
+        wtf4 = sym wtf3 ∙ wtf2
+      in sym wtf4
 
---     lol : true ≡ false
---     lol = ap (λ f → f true) bogus
+    lol : true ≡ false
+    lol = ap (λ f → f true) bogus
 ```
 
 ## 3.2 Propositions as types?
@@ -305,4 +317,26 @@ lemma3∙9∙1 {P} prop = lemma3∙3∙3 prop prop2 ∣_∣ g
         postulate
           -- TODO: Finish this 
           admit : x ≡ y
+```
+
+## 3.11 Contractibility
+
+### Definition 3.11.1
+
+```
+isContr : (A : Set) → Set
+isContr A = Σ A (λ a → (x : A) → a ≡ x)
+```
+
+### Lemma 3.11.8
+
+```
+lemma3∙11∙8 : (A : Set) → (a : A) → isContr (Σ A (λ x → a ≡ x))
+lemma3∙11∙8 A a = (a , refl) , λ y → Σ-≡ (Σ.snd y , helper y)
+  where
+    f : (x : A) → Set
+    f x = a ≡ x
+
+    helper : (y : Σ A f) → transport f (Σ.snd y) refl ≡ Σ.snd y
+    helper y = {!   !}
 ```
\ No newline at end of file
diff --git a/src/HottBook/Chapter4.lagda.md b/src/HottBook/Chapter4.lagda.md
index 6011e70..1bcb079 100644
--- a/src/HottBook/Chapter4.lagda.md
+++ b/src/HottBook/Chapter4.lagda.md
@@ -3,6 +3,7 @@ module HottBook.Chapter4 where
 
 open import HottBook.Chapter1
 open import HottBook.Chapter2
+open import HottBook.Chapter2Exercises
 open import HottBook.Chapter3
 
 private
@@ -26,10 +27,33 @@ record satisfies-equivalence-properties {A B : Set} {f : A → B} (isequiv : (A
 
 ```
 lemma4∙1∙1 : {A B : Set} → (f : A → B) → qinv f → qinv f ≃ ((x : A) → x ≡ x)
-lemma4∙1∙1 {A} f q = {!   !}
+lemma4∙1∙1 {A} {B} f f-qinv = goal
   where
-    ff : qinv f → (x : A) → x ≡ x
-    ff = {!   !}
+    open axiom2∙10∙3
+
+    f-equiv : A ≃ B
+    f-equiv = f , qinv-to-isequiv f-qinv
+
+    p : A ≡ B
+    p = ua f-equiv
+
+    useful : idtoeqv p ≡ f-equiv
+    useful = propositional-computation f-equiv
+
+    goal : qinv f ≃ ((x : A) → x ≡ x)
+
+    goal2 : qinv (Σ.fst (idtoeqv p)) ≃ ((x : A) → x ≡ x)
+    goal = idtoeqv (ap qinv (ap Σ.fst (sym useful)) ∙ ua goal2)
+
+    goal3 : (A : Set) → qinv id ≃ ((x : A) → x ≡ x)
+    goal2 = J (λ A B p → qinv (Σ.fst (idtoeqv p)) ≃ ((x : A) → x ≡ x))
+      (λ A → goal3 A) A B p
+
+    goal4 : (A : Set) → qinv id → Σ (A → A) (λ g → (g ≡ id) × (g ≡ id))
+    goal4 A (mkQinv g α β) = g , funext α , funext β
+
+    goal5 : (A : Set) → Σ (A → A) (λ g → (g ≡ id) × (g ≡ id)) → Σ (Σ (A → A) (λ g → g ≡ id)) (λ h → Σ.fst h ≡ id)
+    goal5 A g = (Σ.fst exercise2∙10) g
 ```
 
 ### Lemma 4.1.2