auto gitdoc commit

2024-04-25 19:39:14 +00:00 · 2024-04-25 19:39:14 +00:00 · 72a46d4f26
commit 72a46d4f26
parent cc73889956
1 changed files with 1 additions and 1 deletions
--- a/src/HottBook/Chapter2Exercises.lagda.md
+++ b/src/HottBook/Chapter2Exercises.lagda.md
@ -63,7 +63,7 @@ exercise2∙13 = aux1 , equiv1

    equiv1 : isequiv aux1
    g equiv1 = rev
-    g-id equiv1 (f , f-equiv @ (mkIsEquiv g g-id h h-id)) =
+    g-id equiv1 e@(f , f-equiv @ (mkIsEquiv g g-id h h-id)) =
      -- proving that given any equivalence e, that:
      --   ((aux1 ∘ rev) e ≡ id e)
      --   (rev (aux1 e) ≡ e)