Let be the relation of being homotopic (for example between morphisms in the category Top). Let and be two morphisms. We say that is a left homotopy inverse to or that is a right homotopy inverse to if . A homotopy inverse of is a map which is simultaneously a left and a right homotopy inverse to .
is said to be a homotopy equivalence if it has a left and a right homotopy inverse. In that case we can choose the left and right homotopy inverses of to be equal. To show this denote by the left and by the right homotopy inverse of . Then
Hence
therefore is not only a left, but also a right, homotopy inverse to .
This makes sense in any category equipped with an equivalence relation , which is compatible with the composition (and with the equality of morphisms).
A functor which is an equivalence of categories is/has a homotopy inverse with respect to the notion of homotopy given by natural isomorphisms.
A weak homotopy equivalence of topological spaces between CW-complexes is a homotopy equivalence and hence has a homotopy inverse.
A weak homotopy equivalence of simplicial sets between Kan complexes is a homotopy equivalence and hence has a homotopy inverse.