From e41548a6f9464b494e3ceee3fd2628391dc6c323 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Tue, 30 Jul 2024 09:29:03 -0500 Subject: [PATCH] update --- src/HottBook/Chapter1.lagda.md | 2 +- src/HottBook/Chapter2.lagda.md | 77 ++++++++++++++++--------- src/HottBook/Chapter2Exercises.lagda.md | 8 ++- src/HottBook/Chapter3.lagda.md | 10 ++-- src/HottBook/Chapter6.lagda.md | 36 ++++++++++-- src/HottBook/Chapter6Exercises.lagda.md | 5 +- 6 files changed, 96 insertions(+), 42 deletions(-) diff --git a/src/HottBook/Chapter1.lagda.md b/src/HottBook/Chapter1.lagda.md index 27b6456..3560e27 100644 --- a/src/HottBook/Chapter1.lagda.md +++ b/src/HottBook/Chapter1.lagda.md @@ -200,7 +200,7 @@ _∘_ : {l1 l2 l3 : Level} {A : Set l1} {B : Set l2} {C : Set l3} → A → C _∘_ g f x = g (f x) -composite-assoc : {A B C D : Set} +composite-assoc : {A B C D : Set l} → (f : A → B) → (g : B → C) → (h : C → D) diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index fba3dab..a0bf5ac 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -88,38 +88,38 @@ module lemma2∙1∙4 {l : Level} {A : Set l} where ### Theorem 2.1.6 (Eckmann-Hilton) ``` -module theorem2∙1∙6 where - Ω-type : (A : Set) → (a : A) → Set - Ω-type A a = refl {x = a} ≡ refl +-- module theorem2∙1∙6 where +-- Ω-type : (A : Set) → (a : A) → Set +-- Ω-type A a = refl {x = a} ≡ refl - compose1 : {A : Set} {a : A} → fst (Ω (A , a)) → fst (Ω (A , a)) → fst (Ω (A , a)) - compose1 x y = x ∙ y +-- compose1 : {A : Set} {a : A} → fst (Ω (A , a)) → fst (Ω (A , a)) → fst (Ω (A , a)) +-- compose1 x y = x ∙ y - Ω² : {l : Level} → Set* l → Set* l - Ω² {l} = Ω[_] {l = l} 2 +-- Ω² : {l : Level} → Set* l → Set* l +-- Ω² {l} = Ω[_] {l = l} 2 - compose2 : {l : Level} {A : Set l} {a : A} → fst (Ω² (A , a)) → fst (Ω² (A , a)) → fst (Ω² (A , a)) - 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 +-- compose2 : {l : Level} {A : Set l} {a : A} → fst (Ω² (A , a)) → fst (Ω² (A , a)) → fst (Ω² (A , a)) +-- 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 _ +-- _∙ᵣ_ : 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 _ +-- _∙ₗ_ : (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 α β = (α ∙ᵣ _) ∙ (_ ∙ₗ β) +-- 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 = {! x !} +-- 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 = {! !} ``` ### Definition 2.1.7 (pointed type) @@ -450,13 +450,13 @@ module lemma2∙4∙12 where e : isequiv id e = mkIsEquiv id (λ _ → refl) id (λ _ → refl) - sym-equiv : {A B : Set} → (f : A ≃ B) → B ≃ A + sym-equiv : {A B : Set l} → (f : A ≃ B) → B ≃ A sym-equiv {A} {B} (f , eqv) = let (mkQinv g α β) = isequiv-to-qinv eqv in g , qinv-to-isequiv (mkQinv f β α) - trans-equiv : {A B C : Set} → (f : A ≃ B) → (g : B ≃ C) → A ≃ C - trans-equiv {A} {B} {C} (f , f-eqv) (g , g-eqv) = + trans-equiv : {A B C : Set l} → (f : A ≃ B) → (g : B ≃ C) → A ≃ C + trans-equiv {l} {A} {B} {C} (f , f-eqv) (g , g-eqv) = let (mkQinv f-inv f-inv-left f-inv-right) = isequiv-to-qinv f-eqv (mkQinv g-inv g-inv-left g-inv-right) = isequiv-to-qinv g-eqv @@ -484,6 +484,27 @@ module lemma2∙4∙12 where in g ∘ f , qinv-to-isequiv (mkQinv (f-inv ∘ g-inv) forward backward) ``` +### ≃-Reasoning + +``` +module ≃-Reasoning where + infix 1 begin_ + begin_ : {l : Level} {A B : Set l} → (A ≃ B) → (A ≃ B) + begin x = x + + _≃⟨⟩_ : {l : Level} (A {B} : Set l) → A ≃ B → A ≃ B + _ ≃⟨⟩ x≃y = x≃y + + infixr 2 _≃⟨⟩_ step-≃ + step-≃ : {l : Level} (A {B C} : Set l) → B ≃ C → A ≃ B → A ≃ C + step-≃ _ y≃z x≃y = lemma2∙4∙12.trans-equiv x≃y y≃z + syntax step-≃ x y≃z x≃y = x ≃⟨ x≃y ⟩ y≃z + + infix 3 _∎ + _∎ : {l : Level} (A : Set l) → (A ≃ A) + A ∎ = lemma2∙4∙12.id-equiv A +``` + ## 2.5 The higher groupoid structure of type formers ### Definition 2.5.1 diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md index c3874b1..15cde75 100644 --- a/src/HottBook/Chapter2Exercises.lagda.md +++ b/src/HottBook/Chapter2Exercises.lagda.md @@ -7,6 +7,10 @@ open import Agda.Primitive open import HottBook.Chapter1 open import HottBook.Chapter2 open import HottBook.Util + +private + variable + l l2 l3 : Level ``` ## Exercise 2.1 @@ -171,9 +175,9 @@ TODO: Generalizing to dependent functions. ## Exercise 2.10 ``` -exercise2∙10 : {A : Set} {B : A → Set} {C : Σ A B → Set} +exercise2∙10 : (A : Set l) (B : A → Set l2) (C : Σ A B → Set l3) → (Σ A (λ x → Σ (B x) (λ y → C (x , y)))) ≃ Σ (Σ A B) C -exercise2∙10 {A} {B} {C} = f , qinv-to-isequiv (mkQinv g f-g g-f) +exercise2∙10 A B C = f , qinv-to-isequiv (mkQinv g f-g g-f) where f : (Σ A (λ x → Σ (B x) (λ y → C (x , y)))) → Σ (Σ A B) C f (x , (y , cxy)) = (x , y) , cxy diff --git a/src/HottBook/Chapter3.lagda.md b/src/HottBook/Chapter3.lagda.md index 92d1676..8133efb 100644 --- a/src/HottBook/Chapter3.lagda.md +++ b/src/HottBook/Chapter3.lagda.md @@ -437,11 +437,11 @@ module section3∙7 where → rec-trunc Bprop f (∣ a ∣) ≡ f a {-# REWRITE rec-trunc-1 #-} - ind-trunc : {A : Set} → {B : ∥ A ∥ → Set} - → ((x : ∥ A ∥) → isProp (B x)) - → ((a : A) → B (∣ a ∣)) - → (x : ∥ A ∥) → B x - ind-trunc f g x = rec-trunc (f x) (λ a → {! g x !}) x + -- ind-trunc : {A : Set} → {B : ∥ A ∥ → Set} + -- → ((x : ∥ A ∥) → isProp (B x)) + -- → ((a : A) → B (∣ a ∣)) + -- → (x : ∥ A ∥) → B x + -- ind-trunc f g x = rec-trunc (f x) (λ a → {! g x !}) x open section3∙7 public ``` diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md index 35264af..f4cc444 100644 --- a/src/HottBook/Chapter6.lagda.md +++ b/src/HottBook/Chapter6.lagda.md @@ -8,6 +8,7 @@ module HottBook.Chapter6 where open import HottBook.Chapter1 open import HottBook.Chapter2 +open import HottBook.Chapter2Exercises open import HottBook.Chapter3 open import HottBook.Chapter6Circle open import HottBook.CoreUtil @@ -415,16 +416,41 @@ lemma6∙5∙3 A B* @ (B , b₀) = f , qinv-to-isequiv (mkQinv g forward {! !} Susp* : {l : Level} → Set* l → Set* l Susp* (A , a₀) = Susp A , N +Susp-universal-property : {A B : Set l} + → (Susp A → B) ≃ Σ B (λ bₙ → Σ B (λ bₛ → A → bₙ ≡ bₛ)) +Susp-universal-property {l} {A} {B} = f , qinv-to-isequiv (mkQinv g forward backward) + where + f : (Susp A → B) → Σ B (λ bₙ → Σ B (λ bₛ → A → bₙ ≡ bₛ)) + f h = h N , h S , λ a → ap h (merid a) + + g : Σ B (λ bₙ → Σ B (λ bₛ → A → bₙ ≡ bₛ)) → (Susp A → B) + g (hn , hs , hm) sa = rec-Susp hn hs hm sa + + forward : (f ∘ g) ∼ id + forward x = {! refl !} + + backward : (g ∘ f) ∼ id + backward x = {! refl !} + +ap-equiv : {A B : Set l} → (F : Set l → Set l2) → (A ≃ B) → (F A ≃ F B) +ap-equiv F (f , _) = (λ fa → {! !}) , {! !} + lemma6∙5∙4 : {l : Level} → (A* @ (A , a₀) : Set* l) → (B* @ (B , b₀) : Set* l) → Map* {l = l} (Susp* A*) B* ≃ Map* A* (Ω B*) -lemma6∙5∙4 A* B* = f , {! !} +lemma6∙5∙4 {l} A* @ (A , a₀) B* @ (B , b₀) = {! !} where - f : Map* (Susp* A*) B* → Map* A* (Ω B*) - f (f' , p) = {! f'' , ? !} - where - f'' : A* → Ω B* + open ≃-Reasoning + open lemma2∙4∙12 + goal : Map* {l = l} (Susp* A*) B* ≃ Map* A* (Ω B*) + goal = begin + (Map* {l = l} (Susp* A*) B*) ≃⟨ id-equiv _ ⟩ + (Σ (Susp A → B) (λ f → f N ≡ b₀)) ≃⟨ {! !} ⟩ + (Σ (Σ B (λ bₙ → Σ B (λ bₛ → A → bₙ ≡ bₛ))) (λ f → fst f ≡ b₀)) ≃⟨ sym-equiv (exercise2∙10 _ _ _) ⟩ + (Σ B (λ bₙ → Σ B (λ bₛ → A → bₙ ≡ bₛ) × (bₙ ≡ b₀))) ≃⟨ {! !} ⟩ + (Σ B (λ bₙ → Σ B (λ bₛ → A → bₙ ≡ bₛ) × (bₙ ≡ b₀))) ≃⟨ {! !} ⟩ + (Map* A* (Ω B*)) ∎ ``` ## 6.6 Cell complexes diff --git a/src/HottBook/Chapter6Exercises.lagda.md b/src/HottBook/Chapter6Exercises.lagda.md index f96f462..58d272e 100644 --- a/src/HottBook/Chapter6Exercises.lagda.md +++ b/src/HottBook/Chapter6Exercises.lagda.md @@ -2,4 +2,7 @@ {-# OPTIONS --rewriting #-} module HottBook.Chapter6Exercises where -``` \ No newline at end of file + +open import HottBook.Chapter6 +``` +