{X : Type u} →
  [inst : TopologicalSpace X] →
    {x₀ x₁ : X} →
      (p : Path x₀ x₁) →
        (f : ↑unitInterval → ↑unitInterval) →
          (hf : Continuous f) → (hf₀ : f 0 = 0) → (hf₁ : f 1 = 1) → p.Homotopy (p.reparam f hf hf₀ hf₁)