auto gitdoc commit

2024-04-22 02:36:11 +00:00 · 2024-04-22 02:36:11 +00:00 · 402ddc0bda
commit 402ddc0bda
parent ff844789bf
1 changed files with 6 additions and 2 deletions
--- 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