auto gitdoc commit

2024-04-22 03:41:28 +00:00 · 2024-04-22 03:41:28 +00:00 · 6bce930a23
commit 6bce930a23
parent 99100fdda1
1 changed files with 3 additions and 1 deletions
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@ -401,7 +401,9 @@ theorem2∙13∙1 m n = encode m n , equiv
        what4 = isequiv.g (Σ.snd what3)
        what5 = what4 tt
      in what5
-    backward (suc m) (suc n) c = {!   !}
+    backward (suc m) (suc n) c =
+      let
+      in {!   !}

    equiv = record
      { g = decode m n