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

hmm

Browse source
This commit is contained in:
Michael Zhang 2023-05-15 14:29:43 -05:00
parent 9716b4b69b
commit f34cb844a4
1 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/2023-05-15-equiv-try-again.agda
View file

@ -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