z
This commit is contained in:
parent
565a7b19d9
commit
bd73915149
|
@ -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
|
||||||
|
```
|
||||||
?
|
?
|
||||||
```
|
```
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue