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