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 theory^{} without the new homotopy type theory features to formalize mathematics, such as the recent formalization of the Feit–Thompson odd-order theorem^{} in Coq [1].
But the traditional view is that mathematics is founded on set theory^{}, 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 structure^{} 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 types^{}” 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 component^{} is contractible^{}, i.e. those which are homotopy equivalent to a discrete space. It is a theorem that the category^{} 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 supports^{} 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 theory^{} 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 isomorphic^{} structures, while higher inductive types allow direct descriptions of objects by their universal properties^{}. 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.
References
- 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
Title | Sets in univalent foundations |
---|---|
\metatable |