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 ${\sum }_{(f:A\to B)}\parallel \mathrm{𝗊𝗂𝗇𝗏}(f)\parallel$; 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 $\mathrm{𝗂𝗌𝖢𝗈𝗇𝗍𝗋}(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.

The fact that every function is equivalent to a fibration is a standard fact in homotopy theory.The notion of object classifierin $(\mathrm{\infty },1)$-categorytheory (the categorical analogue of Theorem 4.8.3 (http://planetmath.org/48theobjectclassifier#Thmprethm1)) is due to Rezk (see [2],[1]).

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.