2-simplex and some more results

src/AdittionalTopics/SimplicialHoTT.lagda.md

@@ -0,0 +1,30 @@
+---
+title: Simplicial HoTT
+---
+
+# Simplicial HoTT
+
+The 2-simplex can be postulated internally in HoTT.
+
+```agda
+module AdittionalTopics.SimplicialHoTT where
+
+open import Chapter11.Exercises public
+```
+
+## Definition of the 2-Simplex
+
+```agda
+postulate
+  Δ² : 𝒰₀
+  isSet-Δ² : isSet Δ²
+  Δ²₀ Δ²₁ : Δ²
+  _Δ²-≤_ : Δ² → Δ² → Prop𝒰 lzero
+  Δ²₀≤Δ²₀ : pr₁ (Δ²₀ Δ²-≤ Δ²₁)
+  Δ²₀≤Δ²₁ : pr₁ (Δ²₀ Δ²-≤ Δ²₁)
+  Δ²₁≤Δ²₀ : ¬ (pr₁ (Δ²₀ Δ²-≤ Δ²₁))
+  Δ²₁≤Δ²₁ : pr₁ (Δ²₀ Δ²-≤ Δ²₁)
+
+ΔHom : {𝒾 : Level} (A : 𝒰 𝒾) (a b : A) → 𝒰 𝒾
+ΔHom A a b = Σ f ꞉ (Δ² → A) , (f Δ²₀ ≡ a) × (f Δ²₁ ≡ b)  
+```

src/Chapter2/Exercises.lagda.md

@@ -46,22 +46,6 @@ _∙₄_ {x = x} p q = tr (λ - → x ≡ -) q p
   → p ∙ q ≡ p ∙₄ q
 ∙₁≡∙₄ (refl _) (refl _) = refl _
 
--- Exercise 2.4
--- The nth dimensional path is the third datum while the boundary are the first
--- two, if needed we can extract the boundary.
-nth-path : (A : 𝒰 𝒾) → ℕ → 𝒰 𝒾
-nth-path A 0 = A
-nth-path A 1 = Σ x ꞉ A , Σ y ꞉ A , x ≡ y
-nth-path A (succ (succ n)) =
-  Σ p ꞉ (nth-path A (succ n)) , Σ q ꞉ (nth-path A (succ n)) , p ≡ q
-
-n+1th-path-boundary :
-    (A : 𝒰 𝒾) (n : ℕ)
-  → nth-path A (succ n)
-  → (nth-path A n × nth-path A n)
-n+1th-path-boundary A 0 (x , y , p) = (x , y)
-n+1th-path-boundary A (succ n) (p , q , h) = p , q
-
 -- Exercise 2.10
 Σ-assoc : {A : 𝒰 𝒾} {B : A → 𝒰 𝒿} (C : (Σ x ꞉ A , B x) → 𝒰 𝓀)
         → (Σ x ꞉ A , (Σ y ꞉ B x , C (x , y))) ≃ (Σ p ꞉ (Σ x ꞉ A , B x) , C p)

src/Chapter3/Book.lagda.md

@@ -211,7 +211,11 @@ isProp-isProp A f g =
 ```agda
 -- Equation 3.4.1.
 LEM : (𝒾 : Level) → 𝒰 (𝒾 ⁺)
-LEM (𝒾) = (A : 𝒰 𝒾) → isProp A → A ⊎ ¬ A
+LEM 𝒾 = (A : 𝒰 𝒾) → isProp A → A ⊎ ¬ A
+
+-- Equation 3.4.1.
+RAA : (𝒾 : Level) → 𝒰 (𝒾 ⁺)
+RAA 𝒾 = (A : 𝒰 𝒾) → isProp A → ¬¬ A → A
 
 -- Definition 3.4.3.
 isDecidable : 𝒰 𝒾 → 𝒰 𝒾
@@ -288,7 +292,15 @@ postulate
 ## 3.8 The axiom of choice
 
 ```agda
---
+-- Definition 3.8.1.
+AC :
+    (X : 𝒰 𝒾) (A : X → 𝒰 𝒿) (P : (x : X) → A x → 𝒰 𝓀)
+  → isSet X → ((x : X) → isSet (A x))
+  → ((x : X) (a : A x) → isProp (P x a))
+  → 𝒰 (𝒾 ⊔ 𝒿 ⊔ 𝓀)
+AC X A P _ _ _ =
+    ((x : X) → ∥ Σ a ꞉ A x , (P x a) ∥)
+  → ∥ Σ g ꞉ ((x : X) → A x) , ((x : X) → P x (g x)) ∥
 ```
 
 ## 3.9 The principle of unique choice

src/Chapter3/Exercises.lagda.md

@@ -83,7 +83,7 @@ isProp⇒isProp-isDecidible' A B f g c (inr b) (inl a) =
 isProp⇒isProp-isDecidible' A B f g c (inr b) (inr b') =
   ap inr (g b b')
 
--- Exercise 3.8.
+-- Exercise 3.9.
 LEM→Prop𝒰≃𝟚 : {𝒾 : Level} → LEM 𝒾 → (Prop𝒰 𝒾 ≃ 𝟚)
 LEM→Prop𝒰≃𝟚 {𝒾} LEM-holds =
   (Prop𝒰→𝟚 , invs⇒equivs Prop𝒰→𝟚 (𝟚→Prop𝒰 , ε , η))
@@ -165,6 +165,20 @@ Prop𝒰≃𝟚→LEM {𝒾} Prop𝒰𝒾≃𝟚 P isProp-P =
      absurd : (im𝟙 ≡ im𝟘) → Raised 𝒾 𝟘
      absurd p = tr id  (ap pr₁ (≃-→-cancel Prop𝒰𝒾≃𝟚 p)) (raise ⋆)
 
+-- Exercise 3.18.
+LEM→RAA : {𝒾 : Level} → LEM 𝒾 → RAA 𝒾
+LEM→RAA f A isProp-A nnA = lemma (f A isProp-A)
+  where
+    lemma : A ⊎ ¬ A → A
+    lemma (inl x) = x
+    lemma (inr x) = !𝟘 A (nnA x)
+
+RAA→LEM : {𝒾 : Level} → RAA 𝒾 → LEM 𝒾
+RAA→LEM f A isProp-A =
+  f (A ⊎ ¬ A)
+    (isProp⇒isProp-isDecidible A isProp-A)
+    (λ g → g (inr (λ a → g (inl a))))
+
 -- Exercise 3.20.
 isContr-Σ⇒fiber-base : {A : 𝒰 𝒾} (P : A → 𝒰 𝒿)
                      → ((a , f) : isContr A)