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