auto gitdoc commit

2024-04-22 03:14:01 +00:00 · 2024-04-22 03:14:01 +00:00 · 49cda94b51
commit 49cda94b51
parent 9ff5bcc30b
1 changed files with 1 additions and 1 deletions
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@ -380,5 +380,5 @@ theorem2∙13∙1 m n = {!   !}

    decode : (m n : ℕ) → code m n → m ≡ n
    decode zero zero c = refl
-    decode (suc m) (suc n) c = {!   !}
+    decode (suc m) (suc n) c = ap suc (decode m n c)
 ```