auto gitdoc commit

2024-04-22 03:44:08 +00:00 · 2024-04-22 03:44:08 +00:00 · 0de6181beb
commit 0de6181beb
parent 46ae45600b
1 changed files with 1 additions and 0 deletions
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@ -404,6 +404,7 @@ theorem2∙13∙1 m n = encode m n , equiv
    backward (suc m) (suc n) c =
      let
        IH = backward m n c
+        what = encode (suc m) (suc n) (decode (suc m) (suc n) c)
      in {!   !}

    equiv = record