diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 212ed30..44967de 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -414,7 +414,7 @@ theorem2∙13∙1 m n = encode m n , equiv
         -- what = transport (λ n → code m n) (decode m n c) (r m)
         what = transport (λ n → code m n) (decode m n c) (r m)
 
-        res2 : transport (λ n → code (suc m) (suc n)) (decode m n c) (r (suc m)) ≡ c
+        res2 : transport (λ x → code (suc m) (suc x)) (decode m n c) (r (suc m)) ≡ c
         res2 = IH
 
         -- res : encode (suc m) (suc n) (ap suc (decode m n c)) ≡ c