rest of 2.3

src/HottBook/Chapter2.lagda.md

@@ -3,8 +3,9 @@ module HottBook.Chapter2 where
 
 open import Relation.Binary.PropositionalEquality
 open import Function
+open import Data.Product
+open import Data.Product.Properties
 Type = Set
-transport = subst
 _∙_ = trans
 ```
 
@@ -19,7 +20,32 @@ ap f {x} p = J (λ y p → f x ≡ f y) p refl
 
 ## 2.3 Type families are fibrations
 
-### Lemma 2.3.4 (Dependent Map)
+### Lemma 2.3.1 (Transport)
+
+```
+transport : {A : Type} (P : A → Type) {x y : A} (p : x ≡ y) → P x → P y
+transport P p = J (λ y r → P y) p
+```
+
+### Lemma 2.3.2 (Path lifting property)
+
+```
+lift : {A : Type} (P : A → Type) {x y : A} (u : P x) → (p : x ≡ y)
+  → (x , u) ≡ (y , transport P p u)
+lift {A} P {x} {y} u p =
+  J (λ the what → (x , u) ≡ (the , transport P what u)) p refl
+```
+
+Verifying its property:
+
+```
+lift-prop : {A : Type} (P : A → Type) {x y : A} (u : P x) → (p : x ≡ y)
+  → proj₁ (Σ-≡,≡←≡ (lift P u p)) ≡ p
+lift-prop P u p =
+  J (λ the what → proj₁ (Σ-≡,≡←≡ (lift P u what)) ≡ what) p refl
+```
+
+### Lemma 2.3.4 (Dependent map)
 
 ```
 apd : {A : Type} {P : A → Type} (f : (x : A) → P x) {x y : A} (p : x ≡ y)