more wip on ch 6

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
+## 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 = {!   !}
+```

src/HottBook/Chapter6Exercises.lagda.md

@@ -0,0 +1,3 @@
+```
+module HottBook.Chapter6Exercises where
+```