auto gitdoc commit

2024-04-22 02:42:07 +00:00 · 2024-04-22 02:42:07 +00:00 · f9502897f8
commit f9502897f8
parent 23341ba529
1 changed files with 4 additions and 2 deletions
--- 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