4. Equivalences

We now study in more detail the notion of equivalence of types that was introduced briefly in Β§2.4 (http://planetmath.org/24homotopiesandequivalences). Specifically, we will give several different ways to define a type π—‚π—Œπ–Ύπ—Šπ—Žπ—‚π—β’(f) having the properties mentioned there. Recall that we wanted π—‚π—Œπ–Ύπ—Šπ—Žπ—‚π—β’(f) to have the following properties, which we restate here:

  1. 1.


  2. 2.


  3. 3.

    π—‚π—Œπ–Ύπ—Šπ—Žπ—‚π—β’(f) is a mere proposition.

Here π—Šπ—‚π—‡π—β’(f) denotes the type of quasi-inverses to f:


By function extensionality, it follows that π—Šπ—‚π—‡π—β’(f) is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to the type


We will define three different types having propertiesΒ 1–3, which we call

  • β€’

    half adjoint equivalences,

  • β€’

    bi-invertible maps, and

  • β€’

    contractible functions.

We will also show that all these types are equivalent. These names are intentionally somewhat cumbersome, because after we know that they are all equivalent and have propertiesΒ 1–3, we will revert to saying simply β€œequivalence” without needing to specify which particular definition we choose. But for purposes of the comparisons in this chapter, we need different names for each definition.

Before we examine the different notions of equivalence, however, we give a little more explanation of why a different concept than quasi-invertibility is needed.

Title 4. Equivalences