∀ {X : Type u_4} [inst : TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ℝ),
  γ.truncate t₀ t₁ =
    { toFun := fun s => γ.extend (min (max (↑s) t₀) t₁), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }