Sets in univalent foundations

We have claimed that univalent foundations can eventually serve as a foundation for “all” of mathematics, but so far we have discussed only homotopy theory. Of course, there are many specific examples of the use of type theoryPlanetmathPlanetmath without the new homotopy type theory features to formalize mathematics, such as the recent formalization of the Feit–Thompson odd-order theoremMathworldPlanetmath in Coq [1].

But the traditional view is that mathematics is founded on set theoryMathworldPlanetmath, in the sense that all mathematical objects and constructions can be coded into a theory such as Zermelo–Fraenkel set theory (ZF). However, it is well-established by now that for most mathematics outside of set theory proper, the intricate hierarchical membership structureMathworldPlanetmath of sets in ZF is really unnecessary: a more “structural” theory, such as Lawvere’s Elementary Theory of the Category of Sets [2], suffices.

In univalent foundations, the basic objects are “homotopy typesMathworldPlanetmath” rather than sets, but we can define a class of types which behave like sets. Homotopically, these can be thought of as spaces in which every connected componentMathworldPlanetmathPlanetmathPlanetmath is contractibleMathworldPlanetmath, i.e. those which are homotopy equivalent to a discrete space. It is a theorem that the categoryMathworldPlanetmath of such “sets” satisfies Lawvere’s axioms (or related ones, depending on the details of the theory). Thus, any sort of mathematics that can be represented in an ETCS-like theory (which, experience suggests, is essentially all of mathematics) can equally well be represented in univalent foundations.

This supportsMathworldPlanetmath the claim that univalent foundations is at least as good as existing foundations of mathematics. A mathematician working in univalent foundations can build structures out of sets in a familiar way, with more general homotopy types waiting in the foundational background until there is need of them. For this reason, most of the applications in this book have been chosen to be areas where univalent foundations has something new to contribute that distinguishes it from existing foundational systems.

Unsurprisingly, homotopy theory and category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath are two of these, but perhaps less obvious is that univalent foundations has something new and interesting to offer even in subjects such as set theory and real analysis. For instance, the univalence axiom allows us to identify isomorphicPlanetmathPlanetmath structures, while higher inductive types allow direct descriptions of objects by their universal propertiesMathworldPlanetmath. Thus we can generally avoid resorting to arbitrarily chosen representatives or transfinite iterative constructions. In fact, even the objects of study in ZF set theory can be characterized, inside the sets of univalent foundations, by such an inductive universal property.


  • 1 Georges Gonthier and Andrea Asperti and Jeremy Avigad and Yves Bertot and Cyril Cohen and François Garillot and Stéphane Le Roux and Assia Mahboubi and Russell O’Connor and Sidi Ould Biha and Ioana Pasca and Laurence Rideau and Alexey Solovyev and Enrico Tassi and Laurent Thery. A Machine-Checked Proof of the Odd Order Theorem. In emphInteractive Theorem Proving, .
  • 2 Lawvere,F. William. An elementary theory of the category of sets (long version) with commentary. Reprints in Theory and Applications of Categories, 11:1–35 2005