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

auto gitdoc commit

Browse source
This commit is contained in:
Michael Zhang 2024-04-22 04:23:04 +00:00
parent 83f9e5861d
commit 4e75616580
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -414,7 +414,7 @@ theorem2∙13∙1 m n = encode m n , equiv
-- what = transport (λ n → code m n) (decode m n c) (r m)
what = transport (λ n → code m n) (decode m n c) (r m)
res2 : transport (λ n → code (suc m) (suc n)) (decode m n c) (r (suc m)) ≡ c
res2 : transport (λ x → code (suc m) (suc x)) (decode m n c) (r (suc m)) ≡ c
res2 = IH
-- res : encode (suc m) (suc n) (ap suc (decode m n c)) ≡ c