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 $\mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}(f)$ having the properties mentioned there. Recall that we wanted $\mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}(f)$ to have the following properties, which we restate here:

1. $\mathrm{𝗊𝗂𝗇𝗏}(f)\to \mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}(f)$.

2. $\mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}(f)\to \mathrm{𝗊𝗂𝗇𝗏}(f)$.

3. $\mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}(f)$ is a mere proposition.

Here $\mathrm{𝗊𝗂𝗇𝗏}(f)$ denotes the type of quasi-inverses to $f$:

$$\sum _{g:B\to A}((f\circ g\sim {\mathrm{𝗂𝖽}}_B)\times (g\circ f\sim {\mathrm{𝗂𝖽}}_A)).$$

By function extensionality, it follows that $\mathrm{𝗊𝗂𝗇𝗏}(f)$ is equivalent to the type

$$\sum _{g:B\to A}((f\circ g={\mathrm{𝗂𝖽}}_B)\times (g\circ f={\mathrm{𝗂𝖽}}_A)).$$

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