auto gitdoc commit

src/HottBook/Chapter2.lagda.md

@@ -298,12 +298,21 @@ postulate
 idToEquiv : {A B : Set}
   → (A ≡ B)
   → A ≃ B
-idToEquiv {A} {B} p = {!   !} , equiv
+idToEquiv {A} {B} p = func , equiv
   where
+    func : A → B
+    func a = transport id p a
+
+    func-inv : B → A
+    func-inv b = transport id (sym p) b
+
+    homotopy : (func ∘ func-inv) ∼ id
+    homotopy x = {!  !}
+
     equiv = record
-      { g = {!   !}
+      { g = func-inv
       ; g-id = {!   !}
-      ; h = {!   !}
+      ; h = func-inv
       ; h-id = {!   !}
       }
 ```