diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 841d9dc..ef0ab04 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -405,7 +405,9 @@ theorem2∙13∙1 m n = encode m n , equiv
       let
         IH = backward m n c
         what : code m n
-        what = encode (suc m) (suc n) (ap suc (decode m n c))
+        -- what = encode (suc m) (suc n) (ap suc (decode m n c))
+        -- what = transport (λ n → code (suc m) n) (ap suc (decode m n c)) (r (suc m))
+        what = transport (λ n → code (suc m) (suc n)) (decode m n c) (r (suc m))
         res : what ≡ c
         res = {!   !}
       in {!   !}