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

---
 src/HottBook/Chapter2.lagda.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index e1e43ed..841d9dc 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -404,7 +404,10 @@ theorem2∙13∙1 m n = encode m n , equiv
     backward (suc m) (suc n) c =
       let
         IH = backward m n c
-        what = encode (suc m) (suc n) (decode (suc m) (suc n) c)
+        what : code m n
+        what = encode (suc m) (suc n) (ap suc (decode m n c))
+        res : what ≡ c
+        res = {!   !}
       in {!   !}
 
     equiv = record