From 3807a5759aee43d72405d79f4f06c24d3e170a8c Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Thu, 11 Jul 2024 00:29:39 -0500 Subject: [PATCH] lemma 3.11.3 --- src/HottBook/Chapter3.lagda.md | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md index 50ada78..2a4e8aa 100644 --- a/src/HottBook/Chapter3.lagda.md +++ b/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