lemma 3.11.3

src/HottBook/Chapter3.lagda.md

@@ -401,17 +401,23 @@ module lemma3∙11∙3 where
   iii : {A : Set} → A ≃ 𝟙 → properties A
   iii Aeqv @ (f , mkIsEquiv g g* h h*) = mkProperties p1 p2 p3
     where
-      p1 = g tt , λ x → {! ap g ?  !}
-      p2 = g tt , λ x y → {!   !}
-      p3 = Aeqv
+      alltt : (a b : 𝟙) → a ≡ b
+      alltt tt tt = refl
 
+      p1 = h tt , λ x → ap h (alltt tt (f x)) ∙ h* x
+      p2 = h tt , λ x y → sym (h* x) ∙ ap h (alltt (f x) (f y)) ∙ h* y
+      p3 = Aeqv
 ```
 
 ### Lemma 3.11.6
 
 ```
 lemma3∙11∙6 : {A : Set} {P : A → Set} → ((a : A) → isContr (P a)) → isContr ((x : A) → P x)
-lemma3∙11∙6 {A} {P} allContr = {!   !}
+lemma3∙11∙6 {A} {P} allContr =
+  let
+    Pa-isProp : isProp ((x : A) → P x)
+    Pa-isProp = example3∙6∙2 λ x → Σ.snd (lemma3∙11∙3.properties.ii (lemma3∙11∙3.i (allContr x)))
+  in {!   !} , {!   !}
 ```
 
 ### Lemma 3.11.8