From 23341ba52999776e5d6666825159cea8b2c6839b Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 22 Apr 2024 02:39:21 +0000
Subject: [PATCH] auto gitdoc commit

---
 src/HottBook/Chapter2.lagda.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 15d6f74..1b01390 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -313,7 +313,10 @@ idToEquiv {A} {B} p = func , equiv
 
         wtf2 : (func ∘ func-inv) ≡ wtf
         wtf2 = refl
-      in {!  !}
+
+        wtf3 : p ∙ (sym p) ≡ refl
+        wtf3 = J {!   !} {!   !} {!   !} {!   !} {!   !}
+      in {!    !}
 
     equiv = record
       { g = func-inv