Subpaths (in topology)

Stream: mathlib4

[Sebastian Kumar]

What do people think about adding a definition for subpaths of a topological path? That is, something like:

import Mathlib

variable {X : Type*} [TopologicalSpace X]

open unitInterval

def subpath {a b : X} (γ : Path a b) (t₀ t₁ : I) : Path (γ t₀) (γ t₁) where
  toFun s := γ ⟨(1 - s) * t₀ + s * t₁,
    (convex_Icc 0 1) t₀.prop t₁.prop (one_minus_nonneg s) s.prop.left (sub_add_cancel 1 _)⟩
  source' := by simp
  target' := by simp

I realize this is similar to Path.truncate, but I think the flexibility of not needing the arguments to be ordered, as well as the alternative definition, make it easier to construct certain homotopies. In particular, I have been using subpaths to formalize the proof that the sphere is simply connected (following Hatcher's "Algebraic Topology"), and the homotopy between(γ.subpath t₀ t₁).trans (γ.subpath t₁ t₂) and γ.subpath t₀ t₂ is very useful for that. Last week I made a pull request with my code at https://github.com/leanprover-community/mathlib4/pull/27261, but this is my first time contributing to Mathlib so I wanted to see what others thought.

PS: I am getting pretty close to finishing the proof that the sphere is simply connected. When that's done, where should it go in Mathlib? Should there be an Instances folder under AlgebraicTopology/FundamentalGroupoid?