From f34cb844a432f7410ea3fc3accc030e7732822a4 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 15 May 2023 14:29:43 -0500
Subject: [PATCH] hmm

---
 src/2023-05-15-equiv-try-again.agda | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/2023-05-15-equiv-try-again.agda b/src/2023-05-15-equiv-try-again.agda
index 9aa1781..5c73269 100644
--- a/src/2023-05-15-equiv-try-again.agda
+++ b/src/2023-05-15-equiv-try-again.agda
@@ -68,14 +68,18 @@ convert-fiber-is-contr y fz i =
     eqv7 = sym eqv6
 
     -- y ≡ convert x
-    ouais = fz
+    sfx = snd fx
+    sfz = snd fz
+
+    what : sfx ≡ ?
+    what = ?
   in
   -- z = fst fz
   -- convert-fiber y ≡ fz
-  -- (x , x₁ ≡ y) ≡ (z , z₁ ≡ y)
+  -- (x , convert x₁ ≡ y) ≡ (z , convert z₁ ≡ y)
   --  - x ≡ z
-  --  - (x₁ ≡ y) ≡ (z₁ ≡ y)
-  eqv7 i , ?
+  --  - (convert x₁ ≡ y) ≡ (convert z₁ ≡ y)
+  eqv7 i , (λ j → ?)
 
 convert-is-equiv : isEquiv convert
 convert-is-equiv .equiv-proof y = convert-fiber y , convert-fiber-is-contr y