auto gitdoc commit

This commit is contained in:
Michael Zhang 2024-04-22 03:55:56 +00:00
parent 9a3b5589b5
commit 662cf3100d

View file

@ -412,7 +412,9 @@ 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)
res : encode (suc m) (suc n) (ap suc (decode m n c)) ≡ c
-- res : encode (suc m) (suc n) (ap suc (decode m n c)) ≡ c
-- res : transport (λ n → code (suc m) n) (ap suc (decode m n c)) (r (suc m)) ≡ c
res : transport (λ n → code (suc m) (suc n)) (decode m n c) (r (suc m)) ≡ c
res = {! !}
in res