From 8658b6a2f5831933bb58effcf7e0e35ef5a3eaab Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Fri, 17 May 2024 19:35:46 -0500
Subject: [PATCH] exercise

---
 src/HottBook/Chapter2.lagda.md          | 66 ++++++++++++++++++++++---
 src/HottBook/Chapter2Exercises.lagda.md | 50 ++++++++++++++++++-
 2 files changed, 107 insertions(+), 9 deletions(-)

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 77684f8..89e05c3 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -315,10 +315,29 @@ Homotopy forms an equivalence relation:
 ### Lemma 2.4.3
 
 ```
--- lemma243 : {A B : Set} {f g : A → B} (H : f ∼ g) {x y : A} (p : x ≡ y)
---   → H x ∙ ap g p ≡ ap f p ∙ H y
--- lemma243 {f} {g} H {x} {y} p =
---   J (λ the what → (H x ∙ ? ≡ ? ∙ H the)) p ?
+lemma2∙4∙3 : {A B : Set} {f g : A → B} (H : f ∼ g) {x y : A} (p : x ≡ y)
+  → H x ∙ ap g p ≡ ap f p ∙ H y
+lemma2∙4∙3 {A} {B} {f} {g} H {x} {y} p = let
+    open ≡-Reasoning
+  in
+  J (λ x1 y1 p1 → (H x1 ∙ ap g p1 ≡ ap f p1 ∙ H y1)) (λ x1 → begin
+    H x1 ∙ ap g refl ≡⟨⟩
+    H x1 ∙ refl ≡⟨ sym (lemma2∙1∙4.i1 (H x1)) ⟩
+    H x1 ≡⟨ lemma2∙1∙4.i2 (H x1) ⟩
+    refl ∙ H x1 ≡⟨⟩
+    ap f refl ∙ H x1 ∎
+  ) x y p
+```
+
+### Corollary 2.4.4
+
+```
+-- lemma2∙4∙4 : {A : Set} {f : A → A} {H : f ∼ id}
+--   → (x : A)
+--   → H (f x) ≡ ap f (H x)
+-- lemma2∙4∙4 {A} {f} {H} x =
+--   let g p = H x in
+--   {!   !}
 ```
 
 ### Definition 2.4.6
@@ -520,12 +539,24 @@ theorem2∙8∙1 x y = func x y , equiv x y
 
 ## 2.9 Π-types and the function extensionality axiom
 
+### Lemma 2.9.1
+
+```
+postulate
+  lemma2∙9∙1 : {A : Set} {B : A → Set}
+    → (f g : (x : A) → B x)
+    → (f ≡ g) ≃ ((x : A) → f x ≡ g x)
+```
+
 ### Lemma 2.9.2
 
 ```
--- happly : {A B : Set} → (f g : A → B) → {x : A} → (p : f ≡ g) → f x ≡ g x
--- happly f g {x} p =
---   J (λ the what → f x ≡ the x) p refl
+happly : {A B : Set}
+  → (f g : A → B)
+  → {x : A} 
+  → (p : f ≡ g)
+  → f x ≡ g x
+happly {A} {B} f g {x} p = ap (λ h → h x) p
 ```
 
 ### Axiom 2.9.3 (Function extensionality)
@@ -538,6 +569,27 @@ postulate
     → f ≡ g
 ```
 
+### Lemma 2.9.6
+
+```
+-- lemma2∙9∙6 : {X : Set} {A B : X → Set} {x y : X}
+--   → (p : x ≡ y)
+--   → (f : A x → B x)
+--   → (g : A y → B y)
+--   → 
+--     let P x = A x → B x in
+--     (transport P p f ≡ g) ≃ ((a : A x) → transport B p (f a) ≡ g (transport A p a))
+-- lemma2∙9∙6 {X} {A} {B} {x} {y} p f g =
+--   let
+--     P x = A x → B x
+
+--     F : (x1 : X) → (f1 : A x1 → B x1) → (g1 : A x1 → B x1) → (transport P refl f1 ≡ g1) → ((a : A x1) → transport B refl (f1 a) ≡ g1 (transport A refl a))
+--     F x f g p a = {! !}
+--   in
+--   J (λ x1 y1 p1 → (f1 : A x1 → B x1) → (g1 : A y1 → B y1) → (transport P p1 f1 ≡ g1) ≃ ((a : A x1) → transport B p1 (f1 a) ≡ g1 (transport A p1 a))) 
+--     (λ x1 f1 g1 → F x1 f1 g1 , qinv-to-isequiv (mkQinv {!   !} {!   !} {!   !})) x y p f g
+```
+
 ## 2.10 Universes and the univalence axiom
 
 ### Lemma 2.10.1
diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md
index f3eb6da..bf8618b 100644
--- a/src/HottBook/Chapter2Exercises.lagda.md
+++ b/src/HottBook/Chapter2Exercises.lagda.md
@@ -1,10 +1,56 @@
 ```
 module HottBook.Chapter2Exercises where
 
+open import Agda.Primitive
 open import HottBook.Chapter1
-open import HottBook.Chapter1Util
 open import HottBook.Chapter2
-open import HottBook.Util
+open import HottBook.Chapter2Lemma221
+```
+
+## Exercise 2.1
+
+Show that the three obvious proofs of Lemma 2.1.2 are pair- wise equal.
+
+```
+module exercise2∙1 {l : Level} {A : Set l} where
+  prf1 : {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
+  prf1 refl q = q
+
+  prf2 : {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
+  prf2 p refl = p
+
+  prf3 : {x y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
+  prf3 refl refl = refl
+
+  prf1≡prf2 : {x y z : A} → prf1 ≡ prf2
+  prf1≡prf2 {x} {y} {z} =
+    let
+      ind p q = J
+        (λ x1 y1 p1 → (q1 : y1 ≡ z) → prf1 p1 q1 ≡ prf2 {x1} {y1} {z} p1 q1)
+        (λ x1 q1 → J (λ x1 z1 q1 → q1 ≡ prf2 refl q1) (λ _ → refl) x1 z q1)
+        x y p q
+    in
+    funext (λ p → funext λ q → ind p q)
+
+  prf2≡prf3 : {x y z : A} → prf2 ≡ prf3
+  prf2≡prf3 {x} {y} {z} =
+    let
+      ind p q = J
+        (λ x1 y1 p1 → (q1 : y1 ≡ z) → prf2 p1 q1 ≡ prf3 {x1} {y1} {z} p1 q1)
+        (λ x1 q1 → J (λ x1 z1 q1 → prf2 refl q1 ≡ prf3 refl q1) (λ _ → refl) x1 z q1)
+        x y p q
+    in
+    funext (λ p → funext λ q → ind p q)
+
+  prf1≡prf3 : {x y z : A} → prf1 ≡ prf3
+  prf1≡prf3 {x} {y} {z} =
+    let
+      ind p q = J
+        (λ x1 y1 p1 → (q1 : y1 ≡ z) → prf1 p1 q1 ≡ prf3 {x1} {y1} {z} p1 q1)
+        (λ x1 q1 → J (λ x1 z1 q1 → q1 ≡ prf3 refl q1) (λ _ → refl) x1 z q1)
+        x y p q
+    in
+    funext (λ p → funext λ q → ind p q)
 ```
 
 ## Exercise 2.4