2.3 lemmas

src/HottBook/Chapter2.lagda.md

@@ -1,4 +1,109 @@
 ```
 module HottBook.Chapter2 where
+
+open import Relation.Binary.PropositionalEquality
+open import Function
+Type = Set
+transport = subst
+_∙_ = trans
 ```
 
+## 2.2 Functions are functors
+
+### Lemma 2.2.1
+
+```
+ap : {A B : Type} (f : A → B) {x y : A} → (x ≡ y) → f x ≡ f y
+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)
+
+```
+apd : {A : Type} {P : A → Type} (f : (x : A) → P x) {x y : A} (p : x ≡ y)
+  → transport P p (f x) ≡ f y
+apd {A} {P} f {x} p =
+  let
+    D : (x y : A) → (p : x ≡ y) → Type
+    D x y p = transport P p (f x) ≡ f y
+
+    d : (x : A) → D x x refl
+    d x = refl
+  in
+  J (λ y p → transport P p (f x) ≡ f y) p (d x)
+```
+
+### Lemma 2.3.5
+
+```
+transportconst : {A : Type} {x y : A} (B : Type) → (p : x ≡ y) → (b : B)
+  → transport (λ _ → B) p b ≡ b
+transportconst {A} {x} B p b =
+  let
+    D : (x y : A) → (p : x ≡ y) → Type
+    D x y p = transport (λ _ → B) p b ≡ b
+
+    d : (x : A) → D x x refl
+    d x = refl
+  in
+  J (λ x p → transport (λ _ → B) p b ≡ b) p (d x)
+```
+
+### Lemma 2.3.8
+
+```
+lemma238 : {A B : Type} (f : A → B) {x y : A} (p : x ≡ y)
+  → apd f p ≡ transportconst B p (f x) ∙ ap f p
+lemma238 {A} {B} f {x} p =
+  J (λ y p → apd f p ≡ transportconst B p (f x) ∙ ap f p) p refl
+```
+
+### Lemma 2.3.9
+
+```
+lemma239 : {A : Type} {P : A → Type} {x y z : A}
+  → (p : x ≡ y) → (q : y ≡ z) → (u : P x)
+  → transport P q (transport P p u) ≡ transport P (p ∙ q) u
+lemma239 {A} {P} p q u =
+  let
+    inner : transport P refl (transport P p u) ≡ transport P p u
+    inner = refl
+
+    ok : p ∙ refl ≡ p
+    ok = J (λ _ r → r ∙ refl ≡ r) p refl
+
+    bruh : transport P (p ∙ refl) u ≡ transport P p u
+    bruh = ap (λ r → transport P r u) ok
+  in
+  J (λ _ what →
+    transport P what (transport P p u) ≡ transport P (p ∙ what) u
+  ) q (inner ∙ sym bruh)
+```
+
+### Lemma 2.3.10
+
+```
+lemma2310 : {A B : Type} (f : A → B) → (P : B → Type)
+  → {x y : A} (p : x ≡ y) → (u : P (f x))
+  → transport (P ∘ f) p u ≡ transport P (ap f p) u
+lemma2310 f P p u =
+  let
+    inner : transport (λ y → P (f y)) refl u ≡ u
+    inner = refl
+  in
+  J (λ _ what → transport (P ∘ f) what u ≡ transport P (ap f what) u) p inner
+```
+
+### Lemma 2.3.11
+
+```
+lemma2311 : {A : Type} {P Q : A → Type} (f : (x : A) → P x → Q x)
+  → {x y : A} (p : x ≡ y) → (u : P x)
+  → transport Q p (f x u) ≡ f y (transport P p u)
+lemma2311 {A} {P} {Q} f {x} {y} p u =
+  J (λ the what → transport Q what (f x u) ≡ f the (transport P what u)) p refl
+```
+
+## 2.4 Homotopies and equivalences

src/HottBook/Chapter2Exercises.lagda.md

@@ -21,23 +21,10 @@ simultaneously with the type of boundaries for such paths.
 
 ## Exercise 2.5
 
-Prove that the functions [2.3.6] and (2.3.7) are inverse equivalences.
+Prove that the functions [2.3.6] and [2.3.7] are inverse equivalences.
 
 [2.3.6]: https://hott.github.io/book/hott-ebook-1357-gbe0b8e2.pdf#equation.2.3.6
 [2.3.7]: https://hott.github.io/book/hott-ebook-1357-gbe0b8e2.pdf#equation.2.3.7
 
 Here is the definition of transportconst from lemma 2.3.5:
 
-```
-transportconst : {A : Type} {x y : A} (B : Type) → (p : x ≡ y) → (b : B)
-  → transport (λ _ → B) p b ≡ b
-transportconst {A} {x} B p b =
-  let
-    D : (x y : A) → (p : x ≡ y) → Type
-    D x y p = transport (λ _ → B) p b ≡ b
-
-    d : (x : A) → D x x refl
-    d x = refl
-  in
-  J (λ x p → transport (λ _ → B) p b ≡ b) p (d x)
-```