auto gitdoc commit

2024-04-22 03:54:12 +00:00 · 2024-04-22 03:54:12 +00:00 · 9a3b5589b5
commit 9a3b5589b5
parent fab11e6119
1 changed files with 4 additions and 3 deletions
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@ -411,9 +411,10 @@ 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)
        what = transport (λ n → code m n) (decode m n c) (r m)
-        res : what ≡ c
-        res = IH
-      in {!   !}
+
+        res : encode (suc m) (suc n) (ap suc (decode m n c)) ≡ c
+        res = {!   !}
+      in res

    equiv = record
      { g = decode m n