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

---
 src/HottBook/Chapter2.lagda.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 82179a6..1681b5b 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -397,6 +397,7 @@ theorem2∙13∙1 m n = encode m n , equiv
       let
         what = encode zero zero refl
         what2 = decode zero zero c
+        third = theorem2∙8∙1 what c
       in {!   !}
     backward (suc m) (suc n) c = {!   !}