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” is usually defined simply as the subspace of the function space consisting of the functions that are homotopy equivalences. In type theory, this would correspond most closely to ; 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 , 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 -category theory (the categorical analogue of Theorem 4.8.3 (http://planetmath.org/48theobjectclassifier#Thmprethm1)) is due to Rezk (see ,).
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.
- 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|