From 36e3186b0f4a35bc5353a0a2e5631179f06f7956 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Fri, 31 May 2024 02:42:25 -0500 Subject: [PATCH] exercise 2.5 --- html/book.toml | 2 +- html/src/SUMMARY.md | 3 ++- src/HottBook/Chapter2.lagda.md | 36 ++++++++++++++++++++----- src/HottBook/Chapter2Exercises.lagda.md | 29 +++++++++++++++++++- 4 files changed, 60 insertions(+), 10 deletions(-) diff --git a/html/book.toml b/html/book.toml index 0a591a2..db499ee 100644 --- a/html/book.toml +++ b/html/book.toml @@ -3,7 +3,7 @@ authors = ["Michael Zhang"] language = "en" multilingual = false src = "src" -title = "HoTT Book" +title = "Research" [preprocessor.katex] macros = "./macros.txt" diff --git a/html/src/SUMMARY.md b/html/src/SUMMARY.md index 6216cdb..03605c5 100644 --- a/html/src/SUMMARY.md +++ b/html/src/SUMMARY.md @@ -24,4 +24,5 @@ # Van Doorn Dissertation -- [Preliminaries](./generated/VanDoornDissertation.Preliminaries.md) \ No newline at end of file +- [Preliminaries](./generated/VanDoornDissertation.Preliminaries.md) +- [HIT](./generated/VanDoornDissertation.HIT.md) \ No newline at end of file diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index 9bd165a..12753e6 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -118,11 +118,15 @@ record pointed (l : Level) : Set (lsuc l) where ### Theorem 2.1.6 (Eckmann-Hilton) -TODO - ``` -Ω² : {l : Level} → pointed l → pointed l -Ω² p = Ω (Ω p) +module theorem2∙1∙6 where + open pointed + + Ω² : {l : Level} → pointed l → pointed l + Ω² p = Ω (Ω p) + + -- compose : {l : Level} → (p : pointed l) → Ω² p + -- compose a b = ? ``` ## 2.2 Functions are functors @@ -222,6 +226,24 @@ transportconst {l₁} {l₂} {A} {x} {y} B p b = J (λ x y p → transport (λ _ → B) p b ≡ b) (λ x → refl) x y p ``` +### Equation 2.3.6 + +``` +equation2∙3∙6 : {A B : Set} {x y : A} {p : x ≡ y} {f : A → B} + → f x ≡ f y + → transport (λ _ → B) p (f x) ≡ f y +equation2∙3∙6 {A} {B} {x} {y} {p} {f} q = transportconst B p (f x) ∙ q +``` + +### Equation 2.3.7 + +``` +equation2∙3∙7 : {A B : Set} {x y : A} {p : x ≡ y} {f : A → B} + → transport (λ _ → B) p (f x) ≡ f y + → f x ≡ f y +equation2∙3∙7 {A} {B} {x} {y} {p} {f} q = sym (transportconst B p (f x)) ∙ q +``` + ### Lemma 2.3.8 ``` @@ -333,10 +355,10 @@ lemma2∙4∙3 {A} {B} {f} {g} H {x} {y} p = let ### Corollary 2.4.4 ``` --- lemma2∙4∙4 : {A : Set} {f : A → A} {H : f ∼ id} +-- corollary2∙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 = +-- corollary2∙4∙4 {A} {f} {H} x = -- let g p = H x in -- {! !} ``` @@ -996,4 +1018,4 @@ theorem2∙15∙2 {X} {A} {B} = mkIsEquiv g (λ _ → refl) g (λ _ → refl) where g : (X → A) × (X → B) → (X → A × B) g (f1 , f2) = λ x → (f1 x , f2 x) -``` \ No newline at end of file +``` \ No newline at end of file diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md index 79a2e41..4ab398d 100644 --- a/src/HottBook/Chapter2Exercises.lagda.md +++ b/src/HottBook/Chapter2Exercises.lagda.md @@ -63,7 +63,11 @@ $A$, simultaneously with the type of boundaries for such paths._ [6]: https://git.mzhang.io/school/type-theory/issues/6 ``` - +data n-dimensional-path {A : Set} : (n : ℕ) → Set where + z : (x y : A) → x ≡ y → n-dimensional-path zero + s : (n : ℕ) → (d : n-dimensional-path {A} n) → n-dimensional-path (suc n) +-- n-dimensional-path {A} zero = (x y : A) → x ≡ y +-- n-dimensional-path {A} (suc n) = {! !} ``` ## Exercise 2.5 @@ -73,6 +77,29 @@ 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 +``` +module exercise2∙5 {A B : Set} {x y : A} {p : x ≡ y} {f : A → B} where + p1 = transportconst B p (f x) + + forward : (q : f x ≡ f y) → equation2∙3∙7 {p = p} (equation2∙3∙6 {p = p} q) ≡ q + forward q = + let + z1 = lemma2∙1∙4.ii1 p1 + z = ap (λ r → r ∙ q) z1 + z2 = lemma2∙1∙4.iv (sym p1) p1 q + z3 = sym (lemma2∙1∙4.i2 q) + in z2 ∙ z ∙ z3 + + backward : (q : transport (λ _ → B) p (f x) ≡ f y) → equation2∙3∙6 {p = p} (equation2∙3∙7 {p = p} q) ≡ q + backward q = + let + z1 = lemma2∙1∙4.ii2 p1 + z2 = ap (λ r → r ∙ q) z1 + z3 = lemma2∙1∙4.iv p1 (sym p1) q + z4 = sym (lemma2∙1∙4.i2 q) + in z3 ∙ z2 ∙ z4 +``` + ## Exercise 2.9 Prove that coproducts have the expected universal property,