theorem 2.15.5

src/HottBook/Chapter2.lagda.md

@@ -976,7 +976,7 @@ theorem2∙15∙2 {X} {A} {B} = mkIsEquiv g (λ _ → refl) g (λ _ → refl)
 ### Equation 2.15.4
 
 ```
-equation2∙15∙4 : {X : Set} {A B : X → Set}
+equation2∙15∙4 : {X : Set l} {A B : X → Set l}
   → ((x : X) → A x × B x)
   → ((x : X) → A x) × ((x : X) → B x)
 equation2∙15∙4 f = ((λ x → Σ.fst (f x)) , λ x → Σ.snd (f x))
@@ -985,6 +985,16 @@ equation2∙15∙4 f = ((λ x → Σ.fst (f x)) , λ x → Σ.snd (f x))
 ### Theorem 2.15.5
 
 ```
--- theorem2∙15∙5 : isequiv equation2∙15∙4
--- theorem2∙15∙5 = qinv-to-isequiv (mkQinv {!   !} {!   !} {!   !})
+theorem2∙15∙5 : {X : Set l} {A B : X → Set l} → isequiv (equation2∙15∙4 {X = X} {A = A} {B = B})
+theorem2∙15∙5 {X = X} {A = A} {B = B} = qinv-to-isequiv (mkQinv g forward backward)
+  where
+    g : ((x : X) → A x) × ((x : X) → B x) → (x : X) → A x × B x
+    g (f , g) x = f x , g x
+
+    forward : (p : ((x : X) → A x) × ((x : X) → B x)) → equation2∙15∙4 (g p) ≡ p
+    forward p = refl
+
+    backward : (f : (x : X) → A x × B x) → g (equation2∙15∙4 f) ≡ f
+    backward f = funext λ x → refl
+      where open axiom2∙9∙3
 ```

src/HottBook/Chapter3.lagda.md

@@ -348,7 +348,7 @@ module definition3∙7∙1 where
 ### Definition 3.8.1
 
 ```
-module axiom-of-choice where
+module definition3∙8∙1 where
   private
     variable
       X : Set
@@ -359,8 +359,16 @@ module axiom-of-choice where
     axiom-of-choice : (prop : (x : X) → (a : A x) → isProp (P x a))
       → ((x : X) → ∥ Σ (A x) (P x) ∥)
       → ∥ Σ ((x : X) → A x) (λ g → (x : X) → P x (g x)) ∥
+open definition3∙8∙1 public
 ```
 
+### Lemma 3.8.2
+
+```
+module lemma3∙8∙2 where
+  definition3∙8∙3 : {X : Set} → (Y : X → Set) → ((x : X) → isSet (Y x)) → ((x : X) → ∥ (Y x) ∥) → ∥ ((x : X) → Y x) ∥
+  definition3∙8∙3 {X} Y allYSet = {!   !}
+```
 
 ## 3.9 The principle of unique choice