From 49cda94b51dfc67acec41716823c613c51ceb6bc Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 22 Apr 2024 03:14:01 +0000
Subject: [PATCH] auto gitdoc commit

---
 src/HottBook/Chapter2.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 8da10c6..204c268 100644
--- 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)
 ```
\ No newline at end of file