# 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 $\mathsf{isequiv}(f)$ having the properties mentioned there. Recall that we wanted $\mathsf{isequiv}(f)$ to have the following properties, which we restate here:

1. 1.

$\mathsf{qinv}(f)\to\mathsf{isequiv}(f)$.

2. 2.

$\mathsf{isequiv}(f)\to\mathsf{qinv}(f)$.

3. 3.

$\mathsf{isequiv}(f)$ is a mere proposition.

Here $\mathsf{qinv}(f)$ denotes the type of quasi-inverses to $f$:

 $\mathchoice{\sum_{g:B\to A}\,}{\mathchoice{{\textstyle\sum_{(g:B\to A)}}}{\sum% _{(g:B\to A)}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}}{\mathchoice{{\textstyle% \sum_{(g:B\to A)}}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}}{% \mathchoice{{\textstyle\sum_{(g:B\to A)}}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)% }}{\sum_{(g:B\to A)}}}\big{(}(f\circ g\sim\mathsf{id}_{B})\times(g\circ f\sim% \mathsf{id}_{A})\big{)}.$

By function extensionality, it follows that $\mathsf{qinv}(f)$ is equivalent to the type

 $\mathchoice{\sum_{g:B\to A}\,}{\mathchoice{{\textstyle\sum_{(g:B\to A)}}}{\sum% _{(g:B\to A)}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}}{\mathchoice{{\textstyle% \sum_{(g:B\to A)}}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}}{% \mathchoice{{\textstyle\sum_{(g:B\to A)}}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)% }}{\sum_{(g:B\to A)}}}\big{(}(f\circ g=\mathsf{id}_{B})\times(g\circ f=\mathsf% {id}_{A})\big{)}.$

We will define three different types having properties 13, 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 13, 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
\metatable