mathlib3

2410c1ff - feat(topology/homotopy): Define homotopy between functions (#8947)

feat(topology/homotopy): Define homotopy between functions (#8947) More PRs are to come, with homotopy between paths etc. So this will probably become a folder at some point, but for now I've just put it in `topology/homotopy.lean`. There's also not that much API here at the moment, more will be added later on.