solve 4.1.1

src/HottBook/Chapter1Util.agda

@@ -5,8 +5,15 @@ open import HottBook.Chapter1
 open import HottBook.Chapter2Lemma231
 open import HottBook.Util
 
+
 Σ-≡ : {l₁ l₂ : Level} {A : Set l₁} {B : A → Set l₂}
   → {p₁ @ (a₁ , b₁) p₂ @ (a₂ , b₂) : Σ A B}
   → Σ (a₁ ≡ a₂) (λ p → transport B p b₁ ≡ b₂)
   → p₁ ≡ p₂
 Σ-≡ {l₁} {l₂} {A} {B} {p₁ @ (a₁ , b₁)} {p₂ @ (a₂ , b₂)} (refl , refl) = refl
+
+Σ-≡' : {l : Level} {A B : Set l}
+  → {p₁ @ (a₁ , b₁) p₂ @ (a₂ , b₂) : A × B}
+  → (a₁ ≡ a₂) × (b₁ ≡ b₂)
+  → p₁ ≡ p₂
+Σ-≡' {p₁ = p₁@(a₁ , b₁)} {p₂ = p₂@(.a₁ , .b₁)} (refl , refl) = refl  

src/HottBook/Chapter3.lagda.md

@@ -603,6 +603,16 @@ lemma3∙11∙8 A a = center , proof
 
     proof : ((x , p) : Σ A (λ x → a ≡ x)) → center ≡ (x , p)
     proof (x , p) = Σ-≡ (p , lemma2∙11∙2.i p refl ∙ sym (lemma2∙1∙4.i2 p))
+
+-- Same thing but flipped :facepalm:
+lemma3∙11∙8' : (A : Set) → (a : A) → isContr (Σ A (λ x → x ≡ a))
+lemma3∙11∙8' A a = center , proof
+  where
+    -- choose center point (a, reflₐ)
+    center = (a , refl)
+
+    proof : ((x , p) : Σ A (λ x → x ≡ a)) → center ≡ (x , p)
+    proof (x , p) = Σ-≡ (sym p , lemma2∙11∙2.ii (sym p) refl ∙ sym (lemma2∙1∙4.i1 (sym (sym p))) ∙ lemma2∙1∙4.iii p)
 ```
 
 ### Lemma 3.11.9
@@ -662,4 +672,4 @@ module lemma3∙11∙10 where
     where
       postulate
         admit : (z : x ≡ y) → f x y ≡ z
-```
+``` 

src/HottBook/Chapter4.lagda.md

@@ -2,6 +2,7 @@
 module HottBook.Chapter4 where
 
 open import HottBook.Chapter1
+open import HottBook.Chapter1Util
 open import HottBook.Chapter2
 open import HottBook.Chapter2Exercises
 open import HottBook.Chapter3
@@ -27,33 +28,67 @@ 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} {B} f f-qinv = goal
+lemma4∙1∙1 {A} {B} f e @ (mkQinv g _ _) = goal
   where
-    open axiom2∙10∙3
+    open Σ
+    open lemma2∙4∙12
+    open axiom2∙9∙3 using (funext)
+    open axiom2∙10∙3 using (ua)
+    open ≡-Reasoning
 
-    f-equiv : A ≃ B
+    fe : A ≃ B
-    f-equiv = f , qinv-to-isequiv f-qinv
+    fe = f , qinv-to-isequiv e
 
     p : A ≡ B
-    p = ua f-equiv
+    p = ua fe
-
+    
-    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)
+    goal2 : ∀ {A B} → (p : A ≡ B) → qinv (idtoeqv p .fst) ≃ ((x : A) → x ≡ x)
-    goal = idtoeqv (ap qinv (ap Σ.fst (sym useful)) ∙ ua goal2)
+    goal = trans-equiv (idtoeqv (ap qinv (ap Σ.fst (sym (axiom2∙10∙3.propositional-computation fe))))) (goal2 p)
 
-    goal3 : (A : Set) → qinv id ≃ ((x : A) → x ≡ x)
+    goal3 : ∀ {A} → qinv id ≃ ((x : A) → x ≡ x)
-    goal2 = J (λ A B p → qinv (Σ.fst (idtoeqv p)) ≃ ((x : A) → x ≡ x))
+    goal2 refl = goal3
-      (λ A → goal3 A) A B p
 
-    goal4 : (A : Set) → qinv id → Σ (A → A) (λ g → (g ≡ id) × (g ≡ id))
+    convert : ∀ {A B} → (f : A → B) → qinv f ≡ Σ (B → A) (λ g → ((f ∘ g) ∼ id) × ((g ∘ f) ∼ id))
-    goal4 A (mkQinv g α β) = g , funext α , funext β
+    convert f = ua ((λ (mkQinv g α β) → g , (α , β)) ,
+      qinv-to-isequiv (mkQinv (λ (g , α , β) → mkQinv g α β) (λ _ → refl) λ _ → refl))
 
-    goal5 : (A : Set) → Σ (A → A) (λ g → (g ≡ id) × (g ≡ id)) → Σ (Σ (A → A) (λ g → g ≡ id)) (λ h → Σ.fst h ≡ id)
+    goal4 : ∀ {A} → qinv id ≡ Σ (Σ (A → A) (λ g → g ≡ id)) (λ h → fst h ≡ id)
-    goal5 A g = (Σ.fst exercise2∙10) g
+
+    goal4 {A} = begin
+      qinv id ≡⟨ convert id ⟩
+      Σ (A → A) (λ g → (g ∼ id) × (g ∼ id)) ≡⟨ ap (Σ (A → A)) (funext lemma) ⟩
+      Σ (A → A) (λ g → (g ≡ id) × (g ≡ id)) ≡⟨ ua exercise2∙10 ⟩
+      Σ (Σ (A → A) (λ g → g ≡ id)) (λ h → fst h ≡ id) ∎
+      where
+        lemma : (id' : A → A) → ((id' ∼ id) × (id' ∼ id)) ≡ ((id' ≡ id) × (id' ≡ id))
+        lemma id' = ua (ff , qinv-to-isequiv (mkQinv gg forward backward))
+          where
+            open axiom2∙9∙3
+
+            ff : (id' ∼ id × id' ∼ id) → (id' ≡ id × id' ≡ id)
+            ff (l , r) = funext l , funext r
+
+            gg : (id' ≡ id × id' ≡ id) → (id' ∼ id × id' ∼ id)
+            gg (l , r) = happly l , happly r
+
+            forward : (ff ∘ gg) ∼ id
+            forward (l , r) = Σ-≡' (propositional-uniqueness l , propositional-uniqueness r)
+
+            backward : (gg ∘ ff) ∼ id
+            backward (l , r) = Σ-≡' (propositional-computation l , propositional-computation r)
+      
+    goal5 : ∀ {A} → isContr (Σ (A → A) (λ g → g ≡ id))
+    goal5 {A} = lemma3∙11∙8' (A → A) id
+
+    goal6 : ∀ {A} → Σ (Σ (A → A) (λ g → g ≡ id)) (λ h → fst h ≡ id) ≃ (id ≡ id)
+    goal6 = lemma3∙11∙9.ii goal5
+
+    goal7 : ∀ {A} → (id ≡ id) ≃ ((x : A) → x ≡ x)
+    goal7 = axiom2∙9∙3.happly-equiv
+
+    goal3 = trans-equiv (idtoeqv goal4) (trans-equiv goal6 goal7)
 ```
 
 ### Lemma 4.1.2