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

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

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 0cb18e8..7ced792 100644
--- 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