4.5 On the definition of equivalences

We have shown that all three definitions of equivalence satisfy the three desirable properties and are pairwise equivalent:

 $\mathsf{isContr}(f)\simeq\mathsf{ishae}(f)\simeq\mathsf{biinv}(f).$

(There are yet more possible definitions of equivalence, but we will stop with these three. See http://planetmath.org/node/87824Exercise 3.11 and the exercises in this chapter for some more.) Thus, we may choose any one of them as “the” definition of $\mathsf{isequiv}(f)$. For definiteness, we choose to define

 $\mathsf{isequiv}(f):\!\!\equiv\mathsf{ishae}(f).$

This choice is advantageous for formalization, since $\mathsf{ishae}(f)$ contains the most directly useful data. On the other hand, for other purposes, $\mathsf{biinv}(f)$ is often easier to deal with, since it contains no 2-dimensional paths and its two symmetrical halves can be treated independently. However, for purposes of this book, the specific choice will make little difference.

In the rest of this chapter, we study some other properties and characterizations of equivalences.

 Title 4.5 On the definition of equivalences \metatable