From e2212f7999130414471a5009d9543edf667b09dc Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Sat, 27 Jul 2024 22:20:41 -0500 Subject: [PATCH] update --- html/ProgressHeader.html | 6 +++++- src/HottBook/Chapter2.lagda.md | 21 +++++++++++++++++++-- 2 files changed, 24 insertions(+), 3 deletions(-) diff --git a/html/ProgressHeader.html b/html/ProgressHeader.html index d8d931b..5ee429a 100644 --- a/html/ProgressHeader.html +++ b/html/ProgressHeader.html @@ -28,4 +28,8 @@ } -

HoTT Book Progress

\ No newline at end of file +

HoTT Book Progress

+ +

+ Last 7 days: +

\ No newline at end of file diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index db399be..fba3dab 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -99,10 +99,27 @@ module theorem2∙1∙6 where Ω² {l} = Ω[_] {l = l} 2 compose2 : {l : Level} {A : Set l} {a : A} → fst (Ω² (A , a)) → fst (Ω² (A , a)) → fst (Ω² (A , a)) - compose2 x y = x ∙ y + compose2 x y = horiz x y + where + variable + A : Set l + a b c : A + p q : a ≡ b + r s : b ≡ c + α : p ≡ q + β : r ≡ s + + _∙ᵣ_ : p ≡ q → (r : b ≡ c) → p ∙ r ≡ q ∙ r + α ∙ᵣ refl = sym (lemma2∙1∙4.i1 _) ∙ α ∙ lemma2∙1∙4.i1 _ + + _∙ₗ_ : (q : a ≡ b) → r ≡ s → q ∙ r ≡ q ∙ s + refl ∙ₗ β = sym (lemma2∙1∙4.i2 _) ∙ β ∙ lemma2∙1∙4.i2 _ + + horiz : p ≡ q → r ≡ s → p ∙ r ≡ q ∙ s + horiz α β = (α ∙ᵣ _) ∙ (_ ∙ₗ β) compose2-commutative : {l : Level} {A : Set l} {a : A} (x y : fst (Ω² (A , a))) → compose2 x y ≡ compose2 y x - compose2-commutative {l} {A} {a} x y = {! !} + compose2-commutative {l} {A} {a} x y = {! x !} ``` ### Definition 2.1.7 (pointed type)