Commit 2021-09-10 15:18 2410c1ff

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.