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
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).