This page develops a theory of universes in the structural set theory called SEAR, parallel to the theory of Grothendieck universes for ZF and the theory of a universe in a topos. See also categories in SEAR.
David Roberts: Can we talk about Grothendieck universes or analogous size-related mechanisms? (this is a naive question, since there may be (no need for/obvious way to do) this in a structural set theory that I am unaware of.
Mike Shulman: Universes can be defined in any structural set theory in a fairly straightforward way, modulo the usual translation from “set of sets” to “family of sets.” There is some stuff from a more ETCS-like perspective at universe in a topos; I’m sure that this can be rephrased in SEAR (if you want to take a shot, feel free!).
David Roberts: I’d certainly like to, subject to real-world time constraints. It seems to me that something could be done to the axiom of collection if we had a axiom of universes (for every set there is a universe acting as a universal family for it, or similar).
Mike Shulman: I’m not sure that Collection can really be eliminated using universes, but maybe it can.
David Roberts: Some sketchy thoughts - a universe will be a relation satisfying axioms analogous to those at universe in a topos. There are few points that need translating into SEAR-language first so we can define smallness of a family of sets
Pullback - unless I am mistaken, the appropriate version is this: Given a function , the family should be regarded as the 'pullback' family. This family should be isomorphic to the family . This leads us to wonder how to define two families to be isomorphic.
Dependent product - this is tricker and I’m not going to do that right now.
Fix a family of sets .
Definition: A family is called -small if there is a function such that for the composite relation
A set is called -small if the relation , which holds of and for all elements of , is a -small family.
For ease of language, we define a composite of families to be the composite relation of the two relations defining the families.
Definition: A family of sets is called a universe if the following axioms are satisfied:
There is an optional axiom, given the axiom of infinity from before:
Without this axiom we do not have that universes contain infinite sets.
Given a universe , we want to define a (meta-)category …
Mike Shulman: The main idea of SEAR is that in a well-pointed topos, global elements suffice for everything. In particular, we can usually dispense with families of things and consider only single ones. So here’s a formulation that I think is more in the spirit of SEAR.
Given a family , recall that for we let be a tabulation of . We say that a set is -small (although really, it would be more appropriate to say ”-small”) if there exists a with . Now we say that (equipped with ) is a universe if it satisfies:
The optional axiom is the same:
The first two properties of a universe clearly imply that the -small sets satisfy Axioms 0–2 of SEAR all by themselves. In particular, and are -small, any subset of a -small set is -small, and if and are small then so is . Thus from the additional assumption of the smallness of powersets, we can conclude that if and are small, so is the set of functions from to . It also follows that coproducts and quotient sets preserve smallness. (For a notion of “predicative universe” we would replace the smallness of powersets with the smallness of function sets, and we might have to separately assume smallness of coproducts and quotients, I’m not sure.)
In order to show that the -small sets model SEAR all by themselves, it remains to show:
The -small sets for a universe satisfy the Collection axiom of SEAR.
Let be a -small set and a property as in the Collection axiom. Let be a property such that holds iff holds and is -small. By the Collection axiom for all sets applied to , there exists a set , a function , and a -indexed family of sets satisfying the desired properties: (1) for any , we have and is -small, and (2) for any , if there exists a -small set with , then . Our goal is to replace and by -small sets and with a relation maintaining the truth of these statements.
Now the induced function is surjective, and since is a subset of it is -small. Thus, by the “Collection” property of a universe, there exists a -small set , a surjection and a function such that . We take and the composite as the function ; we claim that the composite relation still satisfies (1) and (2) above. (We have not replaced yet, so this is still an intermediate step.) Property (1) follows since and , while property (2) follows since by construction.
Now consider a tabulation of . Note that for any we have , and therefore in particular is -small by (1). Since is also -small, the “Replacement” property of a universe implies that is also -small. But the family is equivalent to , in the sense that for all , so it also satisfies (1) and (2); thus we can take and .
Note that both the “Replacement” and “Collection” properties of a universe are required to show the SEAR Collection axiom for -small sets. The naming of these two properties appears to be traditional, however. See in particular the book Algebraic Set Theory by Joyal and Moerdijk.
What about families and dependent products? We define a function, considered as a family of sets, to be -small if each of its fibers is. Note that then we can state the Replacement property as “the composite of -small functions is -small.” Now for functions and , the fiber of the dependent product over is the subset of the function set consisting of functions such that . Thus, if and are -small, so is (by the “Replacement” property), and thus so is this fiber. Hence -small functions are closed under dependent products.
Also of interest is the following, which should be compared to the “descent” axiom in Joyal-Moerdijk.
The following are equivalent for a function .
Clearly the third condition implies the second. The second implies the first, since pullbacks have isomorphic fibers. And in the presence of AC, the second implies the third, since the surjection has a section. Thus the difficulty is in showing that the first implies the second.
Suppose that is -small. This means that for any , there exists a and a bijection . Let be the subset of consisting of those triples such that is a bijection , and let and be the projections. Since is -small, is surjective. Define to be a pullback of along , with projections and , and define by (informally speaking) where . Since each is a bijection, makes a pullback of .