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

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

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 4abf69e..6c2b9a7 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -367,6 +367,8 @@ code (suc x) (suc y) = code x y
 
 ### Theorem 2.13.1
 
+_For all $m, n : N$ we have (m = n) \simeq \texttt{code}(m, n)._
+
 ```
 theorem2∙13∙1 : (m n : ℕ) → (m ≡ n) ≃ code m n
 theorem2∙13∙1 m n = encode m n , equiv