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

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

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index e720d8e..4abf69e 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -414,8 +414,9 @@ theorem2∙13∙1 m n = encode m n , equiv
 
         -- res : encode (suc m) (suc n) (ap suc (decode m n c)) ≡ c
         res : transport (λ n → code (suc m) n) (ap suc (decode m n c)) (r (suc m)) ≡ c
-        res = {!   !}
-      in res
+        res = {!    !}
+
+      in {!   !}
 
     equiv = record
       { g = decode m n