school/type-theory
2
0
Fork 0
Code Issues 11 Pull requests Actions Packages Projects 1 Releases Wiki Activity

z

Browse source
This commit is contained in:
Michael Zhang 2023-05-08 21:09:01 -05:00
parent 565a7b19d9
commit e71aa3e060
1 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/2023-05-06-equiv.lagda.md
View file

@ -90,8 +90,11 @@ Bool-id-is-equiv .equiv-proof y .snd y₁ i .fst =
eqv3′ = cong Bool-id-inv eqv2 eqv3′ = cong Bool-id-inv eqv2
give-me-info = ? give-me-info = ?
-- eqv3 : fst y₁ ≡ y -- 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′ = ?
eqv4 = sym eqv3 eqv4 = sym eqv3
-- eqv4 : y ≡ fst y₁ -- 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 a-b = Bool-id-refl y
c-d = y₁ .snd c-d = y₁ .snd
in in
```
-- https://git.mzhang.io/school/cubical/issues/2 Blocked on this issue: https://git.mzhang.io/school/cubical/issues/2
```
? ?
``` ```