diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index 60d1810..2d2833a 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -307,7 +307,9 @@ idToEquiv {A} {B} p = func , equiv func-inv b = transport id (sym p) b homotopy : (func ∘ func-inv) ∼ id - homotopy x = {! !} + homotopy x = + let wtf = transport id (sym p) (transport id p x) in + {! !} equiv = record { g = func-inv