∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁) (f : ↑unitInterval → ↑unitInterval),
  Continuous f → Continuous fun x => p ⟨↑(unitInterval.symm x.1) * ↑x.2 + ↑x.1 * ↑(f x.2), ⋯⟩