From 72a46d4f26f8f644bc2011e0d49175412d1ddf15 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 25 Apr 2024 19:39:14 +0000
Subject: [PATCH] auto gitdoc commit

---
 src/HottBook/Chapter2Exercises.lagda.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md
index 379b4ff..9ce17fb 100644
--- 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)