lemma 3.11.9

src/HottBook/Chapter2.lagda.md

@@ -647,7 +647,7 @@ happly {A} {B} {f} {g} p x = ap (λ h → h x) p
 
 ```
 postulate
-  funext : {A B : Set l}
+  funext : ∀ {l} {A B : Set l}
     → {f g : A → B}
     → ((x : A) → f x ≡ g x)
     → f ≡ g

src/HottBook/Chapter3.lagda.md

@@ -185,8 +185,9 @@ theorem3∙2∙2 double-neg = conclusion
     allsame u v x = rec-⊥ (u x)
 
     postulate
-      allsamef : (u v : ¬ ¬ bool) → u ≡ v
-
+      allsamef : ∀ {l} {bool : Set l} → (u v : ¬ ¬ bool) → u ≡ v
+    -- allsamef {l} {bool} u v = {!  !}
+    
     all-dn-u-same : transport (λ A → ¬ ¬ A) (sym p) u ≡ u
     all-dn-u-same = allsamef (transport (λ A → ¬ ¬ A) (sym p) u) u
 
@@ -324,7 +325,7 @@ lemma3∙9∙1 {P} prop = lemma3∙3∙3 prop prop2 ∣_∣ g
 ### Definition 3.11.1
 
 ```
-isContr : (A : Set) → Set
+isContr : (A : Set l) → Set l
 isContr A = Σ A (λ a → (x : A) → a ≡ x)
 ```
 
@@ -332,11 +333,56 @@ isContr A = Σ A (λ a → (x : A) → a ≡ x)
 
 ```
 lemma3∙11∙8 : (A : Set) → (a : A) → isContr (Σ A (λ x → a ≡ x))
-lemma3∙11∙8 A a = (a , refl) , λ y → Σ-≡ (Σ.snd y , helper y)
+lemma3∙11∙8 A a = center , proof
   where
-    f : (x : A) → Set
-    f x = a ≡ x
+    -- choose center point (a, reflₐ)
+    center = (a , refl)
 
-    helper : (y : Σ A f) → transport f (Σ.snd y) refl ≡ Σ.snd y
-    helper y = {!   !}
+    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))
+```
+
+### Lemma 3.11.9
+
+```
+module lemma3∙11∙9 where
+  i : ∀ {l1 l2} {A : Set l1} {P : A → Set l2} → ((x : A) → isContr (P x)) → Σ A P ≃ A
+  i {l1} {l2} {A} {P} eachContr = Σ.fst , qinv-to-isequiv (mkQinv g (λ _ → refl) backward)
+    where
+      g : A → Σ A P
+      g a = a , Σ.fst (eachContr a)
+
+      backward : (g ∘ Σ.fst) ∼ id
+      backward (x , p) = 
+        let 
+          xContr = eachContr x
+          y : Σ.fst xContr ≡ p
+          y = Σ.snd xContr p
+        in Σ-≡ (refl , y)
+
+  ii : ∀ {l1 l2} {A : Set l1} {P : A → Set l2} → ((a , _) : isContr A) → Σ A P ≃ P a
+  ii {l1} {l2} {A} {P} (a , aContr) = f , qinv-to-isequiv (mkQinv g forward backward)
+    where
+      f : Σ A P → P a
+      f (x , y) = transport P (sym (aContr x)) y
+
+      g : P a → Σ A P
+      g p = a , p
+
+      forward : (p : P a) → transport P (sym (aContr a)) p ≡ p
+      forward p = y (sym (aContr a))
+        where
+          y : (q : a ≡ a) → transport P q p ≡ p
+          y refl = refl
+
+
+      backward : (g ∘ f) ∼ id
+      backward (x , p) = 
+        let
+          lol : a ≡ x
+          lol = aContr x
+        in Σ-≡ (lol , y lol)
+        where
+          y : (q : a ≡ x) → transport P q (transport P (sym q) p) ≡ p
+          y refl = refl
 ```