Coercion of `Path _ _` to a function

Stream: mathlib4

[Yury G. Kudryashov]

WDYT about switching coercion to function of docs#Path, docs#ContinuousMap.Homotopy etc to use extend versions?

[Yury G. Kudryashov]

#xy : I want to talk about $C^r$ homotopies, and our calculus library expects globally defined functions. I can use manifolds here, but this would add lots of dependencies to the file.

[Patrick Massot]

I don’t think it’s reasonable to use the manifold library here.

[Yury G. Kudryashov]

Another option is to make docs#Path.extend return a bundled ContinuousMap so that we can speak about homotopies between these maps etc.