# 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.

The fact that every function is equivalent to a fibration is a standard fact in homotopy theory. The notion of object classifier in $(\infty,1)$-category theory (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.

## References

• 1 Jacob Lurie, Higher topos theory Princeton University Press,2009
• 2 Charles Rezk. Toposes and homotopy toposes. \urlhttp://www.math.uiuc.edu/ rezk/homotopy-topos-sketch.pdf, 2005.
Title Chapter 4 Notes
\metatable