∀ {X : Type u_2} {Y : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x₀ x₁ : X} {p q : Path x₀ x₁}
  (F : p.Homotopy q) (f : C(X, Y)) (x : ↑unitInterval), (⇑f ∘ ⇑F) (0, x) = (p.map ⋯).toContinuousMap x