susp

src/CubicalHott/Chapter6.agda

@@ -4,9 +4,11 @@ module CubicalHott.Chapter6 where
 open import CubicalHott.Prelude
 open import CubicalHott.Chapter3
 open import Cubical.Data.Equality.Conversion
+open import Cubical.HITs.Susp
 open import Cubical.HITs.S1
 open import Cubical.Data.Int
 open import Cubical.Data.Nat
+open import Cubical.Data.Bool
 
 private
   variable
@@ -91,7 +93,6 @@ module lemma632 where
 --     g : isSet Type
 --     g x y p q = J (λ y' p' → (q' : x ≡ y') → p' ≡ q') goal p q
 
-
 -- Corollary 6.10.13
 
 module corollary61013 where

src/CubicalHott/Chapter8.agda

@@ -76,4 +76,19 @@ module section81 where
   -- Lemma 8.1.8
   encode-decode : (x : S¹) → (c : code {l} x) → encode {l} x (decode x c) ≡ c
   encode-decode base c = {!   !}
-  encode-decode (loop i) c = {!   !} 
+  encode-decode (loop i) c = {!   !} 
+
+-- Definition 8.4.1
+
+Type* = Σ Type (λ A → A)
+
+_→*_ : (A B : Type*) → Type
+_→*_ (A , a) (B , b) = Σ (A → B) (λ f → f a ≡ b)
+
+-- Definition 8.4.2
+
+Ω : Type* → Type*
+Ω (X , x) = (x ≡ x) , refl
+
+Ωf : {X Y : Type*} (f : X →* Y) → Type* → Type*
+Ωf (f , f₀) p = {! sym f₀ ∙ ?  !}

src/CubicalHott/Lemma651.agda

@@ -0,0 +1,35 @@
+{-# OPTIONS --cubical #-}
+module CubicalHott.Lemma651 where
+
+open import CubicalHott.Prelude
+open import CubicalHott.Chapter3
+open import Cubical.HITs.Susp
+open import Cubical.HITs.S1
+open import Cubical.Data.Int
+open import Cubical.Data.Nat
+open import Cubical.Data.Bool
+
+-- Lemma 6.5.1
+
+module lemma651 where
+  lemma : Susp Bool ≃ S¹
+  lemma = isoToEquiv (iso f g f-g g-f) where
+    f : Susp Bool → S¹
+    f north = base
+    f south = base
+    f (merid true i) = refl {x = base} i
+    f (merid false i) = loop i
+
+    g : S¹ → Susp Bool
+    g base = north
+    g (loop i) = (merid false ∙ sym (merid true)) i
+
+    f-g : section f g
+    f-g base = refl
+    f-g (loop i) = {!   !}
+
+    g-f : retract f g
+    g-f north = refl
+    g-f south = merid true
+    g-f (merid true i) = {!   !}
+    g-f (merid false i) = {!   !}