auto gitdoc commit

src/HottBook/Chapter2.lagda.md

@@ -390,14 +390,16 @@ theorem2∙13∙1 m n = encode m n , equiv
 
         c : (x : ℕ) → decode x x (r x) ≡ refl
         c zero = refl
-        c (suc x) = 
-          let wtf = c x in
-          {!   !}
+        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 = {! refl  !}
+    backward (suc m) (suc n) c = {!   !}
 
     equiv = record
       { g = decode m n
       ; g-id = forward m n
       ; h = decode m n
-      ; h-id = {!   !}
+      ; h-id = backward m n
       }
 ```