diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 215e1b9..0c43b58 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -382,9 +382,19 @@ theorem2∙13∙1 m n = encode m n , equiv
     decode zero zero c = refl
     decode (suc m) (suc n) c = ap suc (decode m n c)
 
+    forward : (m n : ℕ) → (p : m ≡ n) → (encode m n ∘ decode m n) p ≡ id p
+    forward m n p = J C c m n p
+      where
+        C : (x y : ℕ) → (p : x ≡ y) → Set
+        C x y p = (encode x y ∘ decode x y) p ≡ id p
+
+        c : (x : ℕ) → decode x x (r x) ≡ refl
+        c zero = refl
+        c (suc x) = {!   !}
+
     equiv = record
       { g = decode m n
-      ; g-id = {!   !}
+      ; g-id = forward m n
       ; h = decode m n
       ; h-id = {!   !}
       }