wtf

src/CubicalHott/Lemma651.agda

@@ -17,7 +17,7 @@ module lemma651 where
     f : Susp Bool → S¹
     f north = base
     f south = base
-    f (merid true i) = refl {x = base} i
+    f (merid true i) = base
     f (merid false i) = loop i
 
     g : S¹ → Susp Bool
@@ -26,10 +26,11 @@ module lemma651 where
 
     f-g : section f g
     f-g base = refl
-    f-g (loop i) = {!   !}
+    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) = {!   !}
-    g-f (merid false i) = {!   !}
+    g-f (merid true i) j = merid true (i ∧ j)
+    g-f (merid false i) = {!   !}