of all homotopy types
A universe is a realm within which (some conceived part, naively and virtually all, of) mathematics may be thought of as taking place. Universes can be purely metamathematical, but we can also reflect upon them and bring them into mathematics. There are several different kinds of ‘universes’. For a physical notion of universe see observable universe.
Much of ordinary mathematics can be thought of as taking place inside “the archetypical category SET of sets”. Typically, the properties of are formulated in first-order logic using a set theory such as ZFC or (more directly) ETCS.
We can generalise this from to any other category . Without further assumptions on the category, there is in general very little mathematics that can be formulated inside it, but a few extra properties and structures are usually sufficient to provide something interesting. This is the general topic of internalisation. The attitude to take is that any specific category is merely one model, while a general class of categories is a theory (really a doctrine, or 2-theory?).
The idea of the large category as the universe of mathematics has an analogue in pre-category-theoretic material set theory. The von Neumann universe is the proper class of all well-founded pure sets.
Then itself is the union of all of the .
If set theory is the foundation of mathematics, then the universes above are part of metamathematics rather than mathematics itself. However, we can also look for small categories or sets that exist within set theory and have the properties of a universe.
There is already a hint of this in the hierarchy out of which the von Neumann universe is built. For some values of , might be a sufficiently large and complete collection of sets in which to do ordinary mathematics. From the nPOV, we can instead look at the category of these sets and the functions between them, although it's more common to think about for some cardinal number .
An infinite set is a simple example, as finite mathematics can be done inside it. Going beyond this, a Grothendieck universe is a set within which other infinite sets exist but which is complete under the operations of material set theory that are needed for ordinary mathematics. The structural analogue is a universe in the topos .
In general, we need some axioms to state the existence of such universes; we can think of these as large cardinal axioms. (The existence of an infinite set is the axiom of infinity; the existence of a Grothendieck universe is the existence of an inaccessible cardinal.)
The use of such universes is convenient when we want to work with large categories “as if they were small.” That is, if we redefine “small” to mean “element of some fixed universe,” then the categories of all small structures of some sort will still be sets (rather than proper classes) in the bigger ambient universe, and thus we can for instance form functor categories between them freely. We do sometimes then need a way to “move a category” from one universe to another; see universe enlargement.
In logic, we use reflection principle?s (see Wikipedia) to systematically identify features of our meta-universe and see what is needed to prove the existence of an internal universe with these features.
This follows the following outline:
We assume that we understand a priori what it means to use first-order logic (or some other finitary base logic).
Using this base logic, we can formulate a foundational set theory that describes a meta-universe such as .
Of course, cannot be described from inside itself. But there may be objects in (internal categories) that look like itself.
We add an additional axiom to our set theory stating that such objects, the internal universes, exist. These are then models of our original set theory.
Now we are using a new, stronger set theory; repeat.
Set theory is not the only foundation of mathematics. For example, there are also various foundational type theories?, closely related to structural set theory. Then we have a meta-universe of all types, and we can also add axioms for the existence of internal universes.