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

---
 src/HottBook/Chapter2.lagda.md | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 1b01390..5fcde50 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -309,13 +309,15 @@ idToEquiv {A} {B} p = func , equiv
     homotopy : (func ∘ func-inv) ∼ id
     homotopy x = 
       let
+        p* : A → B
+        p* = transport id p
+
         wtf x = transport id (sym p) (transport id p x)
 
         wtf2 : (func ∘ func-inv) ≡ wtf
         wtf2 = refl
 
-        wtf3 : p ∙ (sym p) ≡ refl
-        wtf3 = J {!   !} {!   !} {!   !} {!   !} {!   !}
+        wtf3 = J (λ A' B' p' → {!   !}) {!   !} A B p
       in {!    !}
 
     equiv = record