diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 204c268..215e1b9 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -369,7 +369,7 @@ code (suc x) (suc y) = code x y
 
 ```
 theorem2∙13∙1 : (m n : ℕ) → (m ≡ n) ≃ code m n
-theorem2∙13∙1 m n = {!   !}
+theorem2∙13∙1 m n = encode m n , equiv
   where
     r : (n : ℕ) → code n n
     r zero = tt
@@ -381,4 +381,11 @@ theorem2∙13∙1 m n = {!   !}
     decode : (m n : ℕ) → code m n → m ≡ n
     decode zero zero c = refl
     decode (suc m) (suc n) c = ap suc (decode m n c)
+
+    equiv = record
+      { g = decode m n
+      ; g-id = {!   !}
+      ; h = decode m n
+      ; h-id = {!   !}
+      }
 ```
\ No newline at end of file