auto gitdoc commit

2024-04-22 02:33:43 +00:00 · 2024-04-22 02:33:43 +00:00 · ff844789bf
commit ff844789bf
parent faf91c288b
1 changed files with 3 additions and 1 deletions
--- 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