diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 44967de..08607df 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -421,7 +421,7 @@ theorem2∙13∙1 m n = encode m n , equiv
         res : transport (λ n → code (suc m) n) (ap suc (decode m n c)) (r (suc m)) ≡ c
         res = {!    !}
 
-      in {!   !}
+      in res
 
     equiv = record
       { g = decode m n