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

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

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 2c2d9cf..ba73ffb 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -401,7 +401,9 @@ theorem2∙13∙1 m n = encode m n , equiv
         what4 = isequiv.g (Σ.snd what3)
         what5 = what4 tt
       in what5
-    backward (suc m) (suc n) c = {!   !}
+    backward (suc m) (suc n) c =
+      let
+      in {!   !}
 
     equiv = record
       { g = decode m n