Chapter 4 Notes

The fact that the space of continuous maps equipped with quasi-inverses has the wrong homotopy typeMathworldPlanetmath to be the “space of homotopy equivalencesMathworldPlanetmath” is well-known in algebraic topology. In that context, the “space of homotopy equivalences” (AB) is usually defined simply as the subspace of the function space (AB) consisting of the functionsMathworldPlanetmath that are homotopy equivalences. In type theoryPlanetmathPlanetmath, this would correspond most closely to (f:AB)𝗊𝗂𝗇𝗏(f); see 3.11.

The first definition of equivalence given in homotopy type theory was the one that we have called 𝗂𝗌𝖢𝗈𝗇𝗍𝗋(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 (,Theorem 4.2.3 ( 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 (,§4.7 ( are well-known in homotopy theory. Most of them were first proven in type theory by Voevodsky.

The fact that every function is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to a fibrationMathworldPlanetmath is a standard fact in homotopy theory. The notion of object classifier in (,1)-category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath (the categorical analogue of Theorem 4.8.3 ( is due to Rezk (see [2],[1]).

Finally, the fact that univalence implies function extensionality (§4.9 ( 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 homotopyMathworldPlanetmath toposes. \url rezk/homotopy-topos-sketch.pdf, 2005.
Title Chapter 4 Notes