# Chapter 4 Notes

The fact that the space of continuous maps equipped with quasi-inverses has the wrong homotopy type  to be the “space of homotopy equivalences  ” is well-known in algebraic topology. In that context, the “space of homotopy equivalences” $(A\simeq B)$ is usually defined simply as the subspace of the function space $(A\to B)$ consisting of the functions  that are homotopy equivalences. In type theory  , this would correspond most closely to $\mathchoice{\sum_{f:A\to B}\,}{\mathchoice{{\textstyle\sum_{(f:A\to B)}}}{\sum% _{(f:A\to B)}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}}{\mathchoice{{\textstyle% \sum_{(f:A\to B)}}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}}{% \mathchoice{{\textstyle\sum_{(f:A\to B)}}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)% }}{\sum_{(f:A\to B)}}}\mathopen{}\left\|\mathsf{qinv}(f)\right\|\mathclose{}$; see http://planetmath.org/node/87824Exercise 3.11.

The first definition of equivalence given in homotopy type theory was the one that we have called $\mathsf{isContr}(f)$, which was due to Voevodsky. The possibility of the other definitions was subsequently observed by various people. The basic theorems about adjoint equivalences such as Lemma 4.2.2 (http://planetmath.org/42halfadjointequivalences#Thmprelem1),Theorem 4.2.3 (http://planetmath.org/42halfadjointequivalences#Thmprethm1) are adaptations of standard facts in higher category theory and homotopy theory. Using bi-invertibility as a definition of equivalences was suggested by André Joyal.

The properties of equivalences discussed in §4.6 (http://planetmath.org/46surjectionsandembeddings),§4.7 (http://planetmath.org/47closurepropertiesofequivalences) are well-known in homotopy theory. Most of them were first proven in type theory by Voevodsky.

Finally, the fact that univalence implies function extensionality (§4.9 (http://planetmath.org/49univalenceimpliesfunctionextensionality)) is due to Voevodsky. Our proof is a simplification of his.

## References

Title Chapter 4 Notes
\metatable