From c6bc5bd9529fee4a1f79b6f49f3bd53c74a0ad28 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Tue, 16 Jul 2024 18:19:39 -0400 Subject: [PATCH] more wip on ch 6 --- src/HottBook/Chapter6.lagda.md | 51 ++++++++++++++++++++++++- src/HottBook/Chapter6Exercises.lagda.md | 3 ++ 2 files changed, 53 insertions(+), 1 deletion(-) create mode 100644 src/HottBook/Chapter6Exercises.lagda.md diff --git a/src/HottBook/Chapter6.lagda.md b/src/HottBook/Chapter6.lagda.md index 3ce993b..ae5952f 100644 --- a/src/HottBook/Chapter6.lagda.md +++ b/src/HottBook/Chapter6.lagda.md @@ -259,7 +259,56 @@ module S² where S² : Set base : S² surf : refl {x = base} ≡ refl + + -- TODO: Define recursion principle open S² hiding (base) ``` -## 6.5 Suspensions \ No newline at end of file +## 6.5 Suspensions + +``` +module Suspension where + private + variable + A : Set l + + postulate + Susp : Set → Set + N : Susp A + S : Susp A + merid : A → (N {A} ≡ S {A}) + + rec-Susp : {B : Set l} → (n s : B) → (m : A → n ≡ s) → Susp A → B + rec-Susp-N : {B : Set l} → (n s : B) → (m : A → n ≡ s) → rec-Susp n s m N ≡ n + rec-Susp-S : {B : Set l} → (n s : B) → (m : A → n ≡ s) → rec-Susp n s m S ≡ s + {-# REWRITE rec-Susp-N #-} + {-# REWRITE rec-Susp-S #-} + + rec-Susp-merid : {B : Set l} (n s : B) → (m : A → n ≡ s) → (a : A) → ap (rec-Susp n s m) (merid a) ≡ m a +open Suspension public +``` + +### Lemma 6.5.1 + +``` +lemma6∙5∙1 : Susp 𝟚 ≃ S¹ +lemma6∙5∙1 = f , qinv-to-isequiv (mkQinv g forward backward) + where + open S¹ + + m : 𝟚 → base ≡ base + m true = refl + m false = loop + + f : Susp 𝟚 → S¹ + f s = rec-Susp base base m s + + g : S¹ → Susp 𝟚 + g s = rec-S¹ N (merid false ∙ sym (merid true)) s + + forward : (f ∘ g) ∼ id + forward x = rec-S¹ {P = λ x → f (g x) ≡ x} refl {! refl !} x + + backward : (g ∘ f) ∼ id + backward x = {! !} +``` diff --git a/src/HottBook/Chapter6Exercises.lagda.md b/src/HottBook/Chapter6Exercises.lagda.md new file mode 100644 index 0000000..5fee9e9 --- /dev/null +++ b/src/HottBook/Chapter6Exercises.lagda.md @@ -0,0 +1,3 @@ +``` +module HottBook.Chapter6Exercises where +``` \ No newline at end of file