auto gitdoc commit

2024-04-22 03:40:44 +00:00 · 2024-04-22 03:40:44 +00:00 · 99100fdda1
commit 99100fdda1
parent a860168968
1 changed files with 4 additions and 2 deletions
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@ -397,8 +397,10 @@ theorem2∙13∙1 m n = encode m n , equiv
      let
        what = encode zero zero refl
        what2 = decode zero zero c
-        third = theorem2∙8∙1 what c
-      in {!   !}
+        what3 = theorem2∙8∙1 what c
+        what4 = isequiv.g (Σ.snd what3)
+        what5 = what4 tt
+      in what5
    backward (suc m) (suc n) c = {!   !}

    equiv = record