diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index ad638ff..82179a6 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -393,7 +393,11 @@ theorem2∙13∙1 m n = encode m n , equiv
         c (suc x) = ap (λ p → ap suc p) (c x)
 
     backward : (m n : ℕ) → (c : code m n) → (decode m n ∘ encode m n) c ≡ id c
-    backward zero zero c = {!   !}
+    backward zero zero c =
+      let
+        what = encode zero zero refl
+        what2 = decode zero zero c
+      in {!   !}
     backward (suc m) (suc n) c = {!   !}
 
     equiv = record