3.8.1

src/HottBook/Chapter3.lagda.md

@@ -315,17 +315,53 @@ example3∙6∙2 {A} {B} allProps = λ f g → funext λ x → allProps x (f x)
 ```
 module section3∙7 where
   postulate
-    ∥_∥ : Set → Set
+    ∥_∥ : Set l → Set l
-    ∣_∣ : {A : Set} → (a : A) → ∥ A ∥
+    ∣_∣ : {A : Set l} → (a : A) → ∥ A ∥
-    witness : {A : Set} → (x y : ∥ A ∥) → x ≡ y → Set
+    witness : {A : Set l} → (x y : ∥ A ∥) → x ≡ y → Set l
 
-    rec-∥_∥ : (A : Set) → {B : Set} → isProp B → (f : A → B)
+    rec-∥_∥ : (A : Set l) → {B : Set l} → isProp B → (f : A → B)
       → Σ (∥ A ∥ → B) (λ g → (a : A) → g (∣ a ∣) ≡ f a)
 open section3∙7 public
 ```
 
 ### Definition 3.7.1
 
+```
+module definition3∙7∙1 where
+  ⊤ = 𝟙
+  _∧_ = _×_
+  _⇒_ : (P Q : Set l) → Set l
+  P ⇒ Q = P → Q
+  _⇔_ = _≡_
+  -- ¬_ : (P : Set l) → Set l
+  -- ¬ P = P → ⊥
+  _∨_ : (P Q : Set l) → Set l
+  P ∨ Q = ∥ P + Q ∥
+  forall' : (A : Set l) → (P : A → Set l) → Set l
+  forall' A P = (x : A) → P x
+  exists' : (A : Set l) → (P : A → Set l) → Set l
+  exists' A P = ∥ Σ A P ∥
+```
+
+## 3.8 The axiom of choice
+
+### Definition 3.8.1
+
+```
+module axiom-of-choice where
+  private
+    variable
+      X : Set
+      A : X → Set
+      P : (x : X) → A x → Set
+
+  postulate
+    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)) ∥
+```
+
+
 ## 3.9 The principle of unique choice
 
 ### Lemma 3.9.1