auto gitdoc commit

2024-04-22 03:36:58 +00:00 · 2024-04-22 03:36:58 +00:00 · 6d899fd08d
commit 6d899fd08d
parent d48ae4c0c8
1 changed files with 5 additions and 1 deletions
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@ -393,7 +393,11 @@ theorem2∙13∙1 m n = encode m n , equiv
        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 = {!   !}
+    backward zero zero c =
+      let
+        what = encode zero zero refl
+        what2 = decode zero zero c
+      in {!   !}
    backward (suc m) (suc n) c = {!   !}

    equiv = record