From 5ed0e3ac96b67965033026a80b6b1bc06f2d5695 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 22 Apr 2024 03:59:19 +0000 Subject: [PATCH] auto gitdoc commit --- src/HottBook/Chapter2.lagda.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index 1238700..e720d8e 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -413,8 +413,7 @@ theorem2∙13∙1 m n = encode m n , equiv 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 : 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 : transport (λ n → code (suc m) n) (ap suc (decode m n c)) (r (suc m)) ≡ c res = {! !} in res