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

auto gitdoc commit

Browse source
This commit is contained in:
Michael Zhang 2024-04-22 03:50:55 +00:00
parent 4fedf3d1a3
commit fab11e6119
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/HottBook/Chapter2.lagda.md
View file

@ -407,9 +407,12 @@ theorem2∙13∙1 m n = encode m n , equiv
what : code m n
-- what = encode (suc m) (suc n) (ap suc (decode m n c))
-- what = transport (λ n → code (suc m) n) (ap suc (decode m n c)) (r (suc m))
what = transport (λ n → code (suc m) (suc n)) (decode m n c) (r (suc m))
-- what = transport (λ n → code (suc m) (suc n)) (decode m n c) (r (suc m))
-- what = transport (λ n → code m n) (decode m n c) (r m)
-- what = transport (λ n → code m n) (decode m n c) (r m)
what = transport (λ n → code m n) (decode m n c) (r m)
res : what ≡ c
res = {! !}
res = IH
in {! !}
equiv = record