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

---
 src/HottBook/Chapter2.lagda.md | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 8b8e3fd..2b98fc7 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -390,14 +390,16 @@ theorem2∙13∙1 m n = encode m n , equiv
 
         c : (x : ℕ) → decode x x (r x) ≡ refl
         c zero = refl
-        c (suc x) = 
-          let wtf = c x in
-          {!   !}
+        c (suc x) = ap (λ p → ap suc p) (c x)
+
+    backward : (m n : ℕ) → (c : code m n) → (decode m n ∘ encode m n) c ≡ id c
+    backward zero zero c = {! refl  !}
+    backward (suc m) (suc n) c = {!   !}
 
     equiv = record
       { g = decode m n
       ; g-id = forward m n
       ; h = decode m n
-      ; h-id = {!   !}
+      ; h-id = backward m n
       }
 ```
\ No newline at end of file