From f10e3a09b9c83d8534466057d40e4fc7e5cde5af Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Fri, 23 Aug 2024 21:02:47 -0500 Subject: [PATCH] wtf --- src/CubicalHott/Lemma651.agda | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/CubicalHott/Lemma651.agda b/src/CubicalHott/Lemma651.agda index 582aec5..325b3c9 100644 --- a/src/CubicalHott/Lemma651.agda +++ b/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) = {! !} \ No newline at end of file + g-f (merid true i) j = merid true (i ∧ j) + g-f (merid false i) = {! !} \ No newline at end of file