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

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

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 2d2833a..15d6f74 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -308,8 +308,12 @@ idToEquiv {A} {B} p = func , equiv
 
     homotopy : (func ∘ func-inv) ∼ id
     homotopy x = 
-      let wtf = transport id (sym p) (transport id p x) in
-      {!  !}
+      let
+        wtf x = transport id (sym p) (transport id p x)
+
+        wtf2 : (func ∘ func-inv) ≡ wtf
+        wtf2 = refl
+      in {!  !}
 
     equiv = record
       { g = func-inv