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

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

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 5fcde50..7294291 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -317,7 +317,7 @@ idToEquiv {A} {B} p = func , equiv
         wtf2 : (func ∘ func-inv) ≡ wtf
         wtf2 = refl
 
-        wtf3 = J (λ A' B' p' → {!   !}) {!   !} A B p
+        wtf3 = J (λ A' B' p' → A' → A') (λ A' → id) A B p
       in {!    !}
 
     equiv = record