# Commit 2021-10-04 15:09 387ff6e3

View on Github →feat(topology/homotopy): add `homotopy_with`

(#9252)
Added `homotopy_with`

as in `HOL-Analysis`

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 .