feat(topology/homotopy): add `homotopy_with` (#9252)
Added `homotopy_with` as in [`HOL-Analysis`](https://isabelle.in.tum.de/library/HOL/HOL-Analysis/Homotopy.html) extending `homotopy`. Furthermore, I've added `homotopy_rel`.
Also rename/moved the file. There is also some refactoring which is part of the suggestions from #9141 .
