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{\U0001d5ca\U0001d5c2\U0001d5c7\U0001d5cf}(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{\U0001d5c2\U0001d5cc\U0001d5a2\U0001d5c8\U0001d5c7\U0001d5cd\U0001d5cb}(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 $(\mathrm{\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 |