From c966fa9b4f3849b3fc7d4ebc15b3e9e36885637b Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Fri, 12 Jul 2024 04:37:26 -0500
Subject: [PATCH] more progress ch4

---
 src/HottBook/Chapter4.lagda.md | 57 +++++++++++++++++++++++++++++-----
 1 file changed, 50 insertions(+), 7 deletions(-)

diff --git a/src/HottBook/Chapter4.lagda.md b/src/HottBook/Chapter4.lagda.md
index 3d5abff..7b08bd2 100644
--- a/src/HottBook/Chapter4.lagda.md
+++ b/src/HottBook/Chapter4.lagda.md
@@ -6,6 +6,7 @@ open import HottBook.Chapter1Util
 open import HottBook.Chapter2
 open import HottBook.Chapter2Exercises
 open import HottBook.Chapter3
+open import HottBook.CoreUtil
 
 private
   variable
@@ -119,16 +120,16 @@ There exist types A and B and a function f : A → B such that qinv( f ) is not
 ```
 theorem4∙1∙3 : ∀ {l} → Σ (Set l) (λ A → Σ (Set l) (λ B → Σ (A → B) (λ f → isProp (qinv f) → ⊥)))
 -- theorem4∙1∙3 {l} = goal
---   where
---     goal : ∀ {l} → Σ (Set l) (λ A → Σ (Set l) (λ B → Σ (A → B) (λ f → isProp (qinv f) → ⊥)))
+  -- where
+  --   goal : ∀ {l} → Σ (Set l) (λ A → Σ (Set l) (λ B → Σ (A → B) (λ f → isProp (qinv f) → ⊥)))
 
---     goal2 : ∀ {l} → Σ (Set l) (λ X → isProp ((x : X) → x ≡ x) → ⊥)
---     goal {l} = Σ.fst (goal2 {l}) , {!   !} , {!   !} , {!   !}
+  --   goal2 : ∀ {l} → Σ (Set l) (λ X → isProp ((x : X) → x ≡ x) → ⊥)
+  --   goal {l} = Σ.fst (goal2 {l}) , {!   !} , {!   !} , {!   !}
 
---     X : ∀ {l} → Set (lsuc l)
---     X {l} = Σ (Set l) (λ A → ∥ Lift 𝟚 ≡ A ∥)
+  --   X : ∀ {l} → Set (lsuc l)
+  --   X {l} = Σ (Set l) (λ A → ∥ Lift 𝟚 ≡ A ∥)
 
---     goal2 {l} = X {l} , ?
+  --   goal2 {l} = X {lsuc l} , ?
 ```
 
 ## 4.2 Half adjoint equivalences
@@ -148,6 +149,17 @@ record ishae {A B : Set} (f : A → B) : Set where
 ### Lemma 4.2.2
 
 ```
+lemma4∙2∙2 : ∀ {A B} 
+  → (f : A → B) → (g : B → A)
+  → (η : (g ∘ f) ∼ id)
+  → (ε : (f ∘ g) ∼ id)
+  → ((x : A) → ap f (η x) ≡ ε (f x)) ≃ ((y : B) → ap g (ε y) ≡ η (g y))
+lemma4∙2∙2 f g η ε = {!   !}
+```
+
+```
+ishae→qinv : {A B : Set} (f : A → B) → ishae f → qinv f
+ishae→qinv f (mkIshae g η ε _) = mkQinv g ε η
 ```
 
 ### Theorem 4.2.3
@@ -169,6 +181,13 @@ theorem4∙2∙3 {A} {B} f (mkQinv g ε η) = mkIshae g' η' ε' τ
     τ x = {!   !}
 ```
 
+### Definition 4.2.4
+
+```
+fib : ∀ {A B} → (f : A → B) → (y : B) → Set
+fib {A = A} f y = Σ A (λ x → f x ≡ y)
+```
+
 ### Definition 4.2.7
 
 ```
@@ -178,6 +197,14 @@ module definition4∙2∙7 where
 
   rinv : ∀ {A B} (f : A → B) → Set
   rinv {A} {B} f = Σ (B → A) (λ g → (f ∘ g) ∼ id)
+open definition4∙2∙7
+```
+
+### Lemma 4.2.9
+
+```
+lemma4∙2∙9 : ∀ {A B} (f : A → B) → qinv f → isContr (linv f) × isContr (rinv f)
+lemma4∙2∙9 f q = ({!   !} , {!   !}) , ({!   !} , {!   !})
 ```
 
 ### Definition 4.2.10
@@ -194,4 +221,20 @@ module definition4∙2∙10 where
 
 ```
 theorem4∙2∙13 : {A B : Set} (f : A → B) → isProp (ishae f)
+```
+
+## 4.3 Bi-invertible maps
+
+### Definition 4.3.1
+
+```
+biinv : {A B : Set} (f : A → B) → Set
+biinv f = linv f × rinv f
+```
+
+### Theorem 4.3.2
+
+```
+theorem4∙3∙2 : ∀ {A B} → (f : A → B) → isProp (biinv f)
+theorem4∙3∙2 f = {!   !}
 ```
\ No newline at end of file