auto gitdoc commit

2024-04-22 04:07:25 +00:00 · 2024-04-22 04:07:25 +00:00 · 02935a5cc1
commit 02935a5cc1
parent c0222459c3
1 changed files with 2 additions and 0 deletions
--- 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