auto gitdoc commit

src/HottBook/Chapter2.lagda.md

@@ -319,28 +319,26 @@ idToEquiv {A} {B} p = func , equiv
     func-inv : B → A
     func-inv b = transport id (sym p) b
 
-    homotopy : (func ∘ func-inv) ∼ id
-    homotopy x = 
-      let
-        p* : A → B
-        p* = transport id p
+    p* : A → B
+    p* = transport id p
 
-        wtf x = transport id (sym p) (transport id p x)
+    wtf3 : A → A
+    wtf3 = J (λ A' B' p' → A → A') (λ A' → {! id  !}) A B p
 
-        wtf2 : (func ∘ func-inv) ≡ wtf
-        wtf2 = refl
+    wtf3-is-id : wtf3 ∼ id
+    wtf3-is-id x = {!  !}
 
-        wtf3 : A → A
-        wtf3 = J (λ A' B' p' → A' → A') (λ A' → id) A B p
+    wtf3-qinv : qinv wtf3
+    wtf3-qinv = record
+      { g = wtf3
+      ; α = λ x → {!   !}
+      ; β = λ x → {!   !}
+      }
 
-        wtf3-qinv : qinv wtf3
-        wtf3-qinv = record
-          { g = wtf3
-          ; α = λ _ → refl
-          ; β = λ _ → refl
-          }
-
-      in {!    !}
+    -- homotopy : (func ∘ func-inv) ∼ id
+    -- homotopy x = 
+    --   let
+    --   in {!    !}
 
     equiv = record
       { g = func-inv