From bd739151498ac02760c4eba1611eebddf34b9f7b Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 8 May 2023 21:09:01 -0500 Subject: [PATCH] z --- src/2023-05-06-equiv.lagda.md | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/2023-05-06-equiv.lagda.md b/src/2023-05-06-equiv.lagda.md index 8fcd82d..a9b163c 100644 --- a/src/2023-05-06-equiv.lagda.md +++ b/src/2023-05-06-equiv.lagda.md @@ -90,8 +90,11 @@ Bool-id-is-equiv .equiv-proof y .snd y₁ i .fst = eqv3′ = cong Bool-id-inv eqv2 give-me-info = ? -- eqv3 : fst y₁ ≡ y + ``` - -- https://git.mzhang.io/school/cubical/issues/1 +Blocked on this issue: https://git.mzhang.io/school/cubical/issues/1 + + ``` eqv4′ = ? eqv4 = sym eqv3 -- eqv4 : y ≡ fst y₁ @@ -118,8 +121,10 @@ Bool-id-is-equiv .equiv-proof y .snd y₁ i .snd j = a-b = Bool-id-refl y c-d = y₁ .snd in + ``` - -- https://git.mzhang.io/school/cubical/issues/2 +Blocked on this issue: https://git.mzhang.io/school/cubical/issues/2 + ``` ? ```