2.12.5

src/HottBook/Chapter1.lagda.md

@@ -1,9 +1,16 @@
+<details>
+  <summary>Imports</summary>
+
 ```
 module HottBook.Chapter1 where
 
 open import Agda.Primitive
 ```
 
+</details>
+
+# 1 Type theory
+
 ## 1.1 Type theory versus set theory
 
 ## 1.2 Function types
@@ -67,7 +74,7 @@ _×_ A B = Σ A (λ _ → B)
 
 ```
 infixl 6 _+_
-data _+_ (A B : Set) : Set where
+data _+_ {l : Level} (A B : Set l) : Set l where
   inl : A → A + B
   inr : B → A + B
 ```
@@ -86,9 +93,9 @@ rec-+ C f g (inr x) = g x
 ```
 
 ```
-data ⊥ : Set where
+data ⊥ {l : Level} : Set l where
 
-rec-⊥ : {C : Set} → (x : ⊥) → C
+rec-⊥ : {l : Level} → {C : Set l} → (x : ⊥ {l}) → C
 rec-⊥ {C} ()
 ```
 
@@ -123,8 +130,8 @@ rec-ℕ C z s (suc n) = s n (rec-ℕ C z s n)
 
 ```
 infix 3 ¬_
-¬_ : {l : Level} (A : Set l) → Set l
-¬ A = A → ⊥
+¬_ : {l : Level} → (A : Set l) → Set l
+¬_ {l} A = A → ⊥ {l}
 ```
 
 ## 1.12 Identity types
@@ -152,6 +159,16 @@ J : {l₁ l₂ : Level} {A : Set l₁}
 J C c x x refl = c x
 ```
 
+Based path induction:
+
+```
+based-path-induction : {l1 l2 : Level} {A : Set l1} (a : A)
+  → (C : (x : A) → (a ≡ x) → Set l2)
+  → (c : C a refl)
+  → (x : A) → (p : a ≡ x) → C x p
+based-path-induction a C c x refl = c
+```
+
 # Exercises
 
 ## Exercise 1.1

src/HottBook/Chapter2.lagda.md

@@ -65,7 +65,7 @@ module ≡-Reasoning where
 ### Lemma 2.1.4
 
 ```
-module lemma2∙1∙4 {A : Set} where
+module lemma2∙1∙4 {l : Level} {A : Set l} where
   i1 : {x y : A} (p : x ≡ y) → p ≡ p ∙ refl
   i1 {x} {y} p = J (λ x y p → p ≡ p ∙ refl) (λ _ → refl) x y p
 
@@ -85,7 +85,7 @@ module lemma2∙1∙4 {A : Set} where
   iv {x} {y} {z} {w} p q r = let
       open ≡-Reasoning
 
-      C : (x y : A) → (p : x ≡ y) → Set
+      C : (x y : A) → (p : x ≡ y) → Set l
       C x y p = (q : y ≡ z) → p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
 
       c : (x : A) → C x x refl
@@ -254,9 +254,9 @@ lemma2∙3∙9 {A} {x} {y} {z} P p q u =
 ### Lemma 2.3.10
 
 ```
-lemma2∙3∙10 : {l : Level} {A B : Set (lsuc l)}
+lemma2∙3∙10 : {l1 l2 : Level} {A B : Set l1}
   → (f : A → B)
-  → (P : B → Set l)
+  → (P : B → Set l2)
   → {x y : A}
   → (p : x ≡ y)
   → (u : P (f x))
@@ -768,32 +768,32 @@ open axiom2∙10∙3
 ### Theorem 2.11.2
 
 ```
-module theorem2∙11∙2 where
+module lemma2∙11∙2 where
   open ≡-Reasoning
 
-  i : {A : Set} {a x1 x2 : A}
+  i : {l : Level} {A : Set l} {a x1 x2 : A}
     → (p : x1 ≡ x2)
     → (q : a ≡ x1)
     → transport (λ y → a ≡ y) p q ≡ q ∙ p
-  i {A} {a} {x1} {x2} p q =
+  i {l} {A} {a} {x1} {x2} p q =
     J (λ x3 x4 p1 → (q1 : a ≡ x3) → transport (λ y → a ≡ y) p1 q1 ≡ q1 ∙ p1)
       (λ x3 q1 → J (λ x5 x6 q2 → transport (λ y → a ≡ y) refl q1 ≡ q1 ∙ refl) (λ x4 → lemma2∙1∙4.i1 q1) a x3 q1)
       x1 x2 p q
 
-  ii : {A : Set} {a x1 x2 : A}
+  ii : {l : Level} {A : Set l} {a x1 x2 : A}
     → (p : x1 ≡ x2)
     → (q : x1 ≡ a)
     → transport (λ y → y ≡ a) p q ≡ sym p ∙ q
-  ii {A} {a} {x1} {x2} p q = 
+  ii {l} {A} {a} {x1} {x2} p q = 
     J (λ x y p → (q1 : x ≡ a) → transport (λ y → y ≡ a) p q1 ≡ sym p ∙ q1)
       (λ x q1 → J (λ x y p → transport (λ y → y ≡ a) refl q1 ≡ sym refl ∙ q1) (λ x → lemma2∙1∙4.i2 q1) x a q1)
       x1 x2 p q
 
-  iii : {A : Set} {a x1 x2 : A}
+  iii : {l : Level} {A : Set l} {a x1 x2 : A}
     → (p : x1 ≡ x2)
     → (q : x1 ≡ x1)
     → transport (λ y → y ≡ y) p q ≡ sym p ∙ q ∙ p
-  iii {A} {a} {x1} {x2} p q =
+  iii {l} {A} {a} {x1} {x2} p q =
     J (λ x y p → (q1 : x ≡ x) → transport (λ y → y ≡ y) p q1 ≡ sym p ∙ q1 ∙ p)
       (λ x q1 → J (λ x y p → transport (λ y → y ≡ y) refl q1 ≡ sym refl ∙ q1 ∙ refl)
         (λ x → let helper = ap (λ p → sym refl ∙ p) (lemma2∙1∙4.i1 q1) in lemma2∙1∙4.i2 q1 ∙ helper)
@@ -845,8 +845,48 @@ theorem2∙11∙4 {A} {B} {f} {g} {a} {a'} p q =
     a a' p q
 ```
 
+### Theorem 2.11.5
+
+```
+-- theorem2∙11∙5 : {A : Set} {a a' : A}
+--   → (p : a ≡ a')
+--   → (q : a ≡ a)
+--   → (r : a' ≡ a')
+--   → (transport (λ y → y ≡ y) p q ≡ r) ≃ (q ∙ p ≡ p ∙ r)
+```
+
 ## 2.12 Coproducts
 
+### Theorem 2.12.5
+
+```
+module 2∙12∙5 {l : Level} {A B : Set l} (a₀ : A) where
+  code : A + B → Set l
+  code (inl a) = a₀ ≡ a
+  code (inr b) = ⊥
+
+  encode : (x : A + B) → (p : inl a₀ ≡ x) → code x
+  encode x p = transport code p refl
+
+  decode : (x : A + B) → code x → inl a₀ ≡ x
+  decode (inl x) c = ap inl c
+
+  backward : (x : A + B) → (c : code x) → encode x (decode x c) ≡ c
+  backward (inl x) c =
+    let open ≡-Reasoning in begin
+      encode (inl x) (decode (inl x) c) ≡⟨⟩
+      transport code (ap inl c) refl ≡⟨ sym (lemma2∙3∙10 inl code c refl) ⟩
+      transport (λ a → a₀ ≡ a) c refl ≡⟨ lemma2∙11∙2.i c refl ⟩
+      refl ∙ c ≡⟨ sym (lemma2∙1∙4.i2 c) ⟩
+      c ∎
+
+  forward : (x : A + B) → (p : inl a₀ ≡ x) → decode x (encode x p) ≡ p
+  forward x p = based-path-induction (inl a₀) (λ x1 p1 → decode x1 (encode x1 p1) ≡ p1) refl x p
+
+  theorem2∙12∙5 : (x : A + B) → (inl a₀ ≡ x) ≃ (code x)
+  theorem2∙12∙5 x = encode x , qinv-to-isequiv (mkQinv (decode x) (backward x) (forward x))
+```
+
 ### Remark 2.12.6
 
 ```

src/HottBook/Primitives.agda

@@ -0,0 +1,21 @@
+module HottBook.Primitives where
+
+{-# BUILTIN TYPE Type  #-}
+{-# BUILTIN SETOMEGA Typeω #-}
+{-# BUILTIN PROP Prop  #-}
+{-# BUILTIN PROPOMEGA Propω #-}
+{-# BUILTIN STRICTSET SType  #-}
+{-# BUILTIN STRICTSETOMEGA STypeω #-}
+
+postulate
+  Level : Type
+  lzero : Level
+  lsuc  : Level → Level
+  _⊔_   : Level → Level → Level
+infixl 6 _⊔_
+
+{-# BUILTIN LEVELUNIV LevelUniv #-}
+{-# BUILTIN LEVEL Level #-}
+{-# BUILTIN LEVELZERO lzero #-}
+{-# BUILTIN LEVELSUC lsuc #-}
+{-# BUILTIN LEVELMAX _⊔_ #-}