add lemma 6.5.1

src/CubicalHott/Lemma6-5-1.agda

@@ -0,0 +1,59 @@
+-- https://mzhang.io/posts/2024-09-18-hcomp/
+
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma6-5-1 where
+
+open import CubicalHott.Prelude
+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
+
+Σ2≃S¹ : Susp Bool ≃ S¹
+Σ2≃S¹ = isoToEquiv (iso f g fg gf) where
+
+  f : Susp Bool → S¹
+  f north = base
+  f south = base
+  f (merid true i) = base
+  f (merid false i) = loop i
+
+  g : S¹ → Susp Bool
+  g base = north
+  g (loop i) = (merid false ∙ sym (merid true)) i
+
+  fg : (s : S¹) → f (g s) ≡ s
+  fg base = refl
+  fg (loop i) j =
+    let
+      u = λ k → λ where
+        (i = i0) → base
+        (i = i1) → f (merid true (~ k))
+        (j = i0) →
+          let u = λ k' → λ where
+            (i = i0) → base
+            (i = i1) → f (merid true (~ k'))
+          in hfill u (inS (f (merid false i))) k
+        (j = i1) → loop i
+    in hcomp u (f (merid false i))
+
+  gf : (b : Susp Bool) → g (f b) ≡ b
+  gf north = refl
+  gf south = merid true
+  gf (merid true i) j = merid true (i ∧ j)
+  gf (merid false i) j =
+    let
+      u = λ k → λ where
+        (i = i0) → north
+        (i = i1) → merid true (j ∨ ~ k)
+        (j = i0) →
+          let u = λ k' → λ where
+            (i = i0) → north
+            (i = i1) → merid true (~ k')
+          in hfill u (inS (merid false i)) k
+        (j = i1) → merid false i
+    in hcomp u (merid false i)

src/CubicalHott/Lemma651.agda

@@ -1,36 +0,0 @@
-{-# 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) = base
-    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) = {! helper  !} where
-      helper : f (g (loop i)) ≡ loop i
-
-    g-f : retract f g
-    g-f north = refl
-    g-f south = merid true
-    g-f (merid true i) j = merid true (i ∧ j)
-    g-f (merid false i) = {!   !}