diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index 8da10c6..204c268 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -380,5 +380,5 @@ theorem2∙13∙1 m n = {! !} decode : (m n : ℕ) → code m n → m ≡ n decode zero zero c = refl - decode (suc m) (suc n) c = {! !} + decode (suc m) (suc n) c = ap suc (decode m n c) ``` \ No newline at end of file