of all homotopy types
To free the notion from membership-based set theory, we must replace sets of sets by families of sets, just as in passing from power sets to power objects we must replace sets of subsets by families of subsets.
A universe in a topos is a morphism satisfying the axioms to follow. We think of as a -indexed family of objects (sets), and we define a morphism (regarded as an -indexed family of objects) to be -small if there exists a morphism and a pullback square
Note that is not, in general, unique: a universe can contain many isomorphic sets. With this definition, the pullback of a -small morphism is automatically again -small. We say that an object is -small if is -small.
The axioms which must be satisfied are:
Every monomorphism is -small.
The composite of -small morphisms is -small.
If and are -small, then so is the dependent product (where is the right adjoint to ).
The subobject classifier is -small.
Note that since is a monomorphism, (1) and (4) imply that the initial object is -small. A predicative universe is a morphism where instead of (4) we assume merely that is -small; this makes sense in any locally cartesian closed category. In a topos, the generic subobject is a predicative universe, and of course a morphism is -small if and only if it is a monomorphism.
If we assume only (1)–(3), then the identity morphism of the initial object would be a universe, for which it itself is the only -small morphism. On the other hand, if has a natural numbers object , we may additionally assume that is -small, to ensure that all universes contain “infinite” sets.
Note that any object isomorphic to a -small object is -small; thus in the language of Grothendieck universes this notion of smallness corresponds to essential smallness. Roughly, we may say that (1) corresponds to transitivity of a Grothendieck universe, (3) and (4) correspond to closure under power sets, and (2) corresponds to closure under indexed unions.
We think of as being the disjoint union over of the . In the language of indexed categories, this is precisely the case: the object is the indexed coproduct of the -indexed family .
By the definition of -smallness and the notation just introduced, an object in , regarded as a -indexed family , is -small precisely if it is isomorphic to one of the .
If is a -small set by the above and if is a monomorphism so that is a subset of , it follows from 1) and 2) that the comoposite is -small, hence that is -small. So: a subset of a -small set is -small.
Let , and be objects of , regarded as -indexed families , and . Notice that is canonically isomorphic to . Since is defined to be the right adjoint to it follows that is the function set of functions from to . By 3), if , are -small then so is the function set .
Let be a -small set, in that is -small, and let be -small, to be thought of as an -indexed family of -small sets , where is the pullback , so that is the disjoint union of the : . By axiom 2) the composite morphism is -small, hence is a -small set, hence the -indexed union of -small sets is -small.
By standard constructions in set theory from these properties the following further closure properties of the universe follow.
the sets are -small;
a subset of a -small set is -small;
the power set of any -small set is -small;
the function set for any two -small sets is -small;
the union of a -small family of -small sets is -small.
the product of a -small family of -small sets is -small.
Just as ZFC and other material set theories may be augmented with axioms guaranteeing the existence of Grothendieck universes, so may ETCS and other structural set theories be augmented with axioms guaranteeing the existence of universes in the above sense. For example, the counterpart of Grothendieck’s axiom
An internal full subcategory of is a full sub-indexed category of (that is, a collection of full subcategories closed under reindexing) such that there exists a generic -morphism, i.e. a morphism in such that for any in , we have for some . In this case (since is locally cartesian closed) there exists an internal category in such that is equivalent, as an indexed category, to the indexed category represented by .
An internal full subcategory is an internal full subtopos if each is a logical subtopos of (closed under finite limits, exponentials, and containing the subobject classifier). A universe in , as defined above, can then be identified with an internal full subtopos satisfying the additional axiom that -small morphisms are closed under composition.
In a topos with a universe, we can talk about small objects in the internal logic by instead talking about elements of . We can then rephrase the axioms of a universe in the internal logic to look more like the usual axioms for a Grothendieck universe, with the morphism interpreted as a “family of objects” :
Mike: I haven’t actually checked anything in this section, but it seems probable.