nLab universes in SEAR

Universes in SEAR

Universes in SEAR

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.

Using families

David Roberts: Some sketchy thoughts - a universe will be a relation UEU \looparrowright E 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 IAI \looparrowright A

  • Pullback - unless I am mistaken, the appropriate version is this: Given a function IUI \to U, the family IEI \looparrowright E should be regarded as the 'pullback' family. This family should be isomorphic to the family IAI \looparrowright A. 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 UEU \looparrowright E.


A family a:IAa:I \looparrowright A is called UU-small if there is a function f:IUf:I \to U such that for the composite relation IEI \looparrowright E

A set AA is called UU-small if the relation 1A\mathbf{1}\looparrowright A, which holds of ** and aa for all elements aa of AA, is a UU-small family.

For ease of language, we define a composite of families to be the composite relation of the two relations defining the families.


A family of sets UEU \looparrowright E is called a universe if the following axioms are satisfied:

  • The composite of two UU-small families is UU-small
  • The relation f o:BAf^o:B\looparrowright A opposite to an injective function f:ABf:A \to B is a UU-small family
  • P1P\mathbf{1} is a UU-small set
  • (Something about dependent products, once these are defined)

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 UEU \looparrowright E, we want to define a (meta-)category Set USet_U

Using mere sets

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 E:UXE:U\looparrowright X, recall that for uUu\in U we let E uE_u be a tabulation of {xX|E(u,x)}X\{x\in X | E(u,x) \}\subseteq X. We say that a set AA is UU-small (although really, it would be more appropriate to say “EE-small”) if there exists a uUu\in U with AE uA\cong E_u. Now we say that UU (equipped with EE) is a universe if it satisfies:

  • There exists an inhabited UU-small set.
  • The tabulation of any relation between two UU-small sets is UU-small.
  • If AA is UU-small, then so is PAP A.
  • (Replacement) If f:ABf:A\to B is a function such that BB is UU-small and for each bBb\in B, the set f 1(b)f^{-1}(b) is UU-small, then AA is UU-small.
  • (Collection) If p:BAp:B\twoheadrightarrow A is a surjective function where AA is UU-small, then there exists a UU-small set CC, a surjection q:CAq:C\twoheadrightarrow A and a function f:CBf:C\to B such that q=pfq = p\circ f.

The optional axiom is the same:

  • There exists an infinite UU-small set (in the sense of Axiom 4).

The first two properties of a universe clearly imply that the UU-small sets satisfy Axioms 0–2 of SEAR all by themselves. In particular, \emptyset and 11 are UU-small, any subset of a UU-small set is UU-small, and if AA and BB are small then so is A×BA\times B. Thus from the additional assumption of the smallness of powersets, we can conclude that if AA and BB are small, so is the set B AB^A of functions from AA to BB. 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 UU-small sets model SEAR all by themselves, it remains to show:


The UU-small sets for a universe UU satisfy the Collection axiom of SEAR.


Let AA be a UU-small set and PP a property as in the Collection axiom. Let PP' be a property such that P(a,X)P'(a,X) holds iff P(a,X)P(a,X) holds and XX is UU-small. By the Collection axiom for all sets applied to PP', there exists a set BB, a function p:BAp:B\to A, and a BB-indexed family of sets M:BYM:B\looparrowright Y satisfying the desired properties: (1) for any bBb\in B, we have P(p(b),M b)P(p(b),M_b) and M bM_b is UU-small, and (2) for any aAa\in A, if there exists a UU-small set XX with P(a,X)P(a,X), then aim(p)a\in im(p). Our goal is to replace BB and YY by UU-small sets BB' and YY' with a relation M:BYM':B'\looparrowright Y' maintaining the truth of these statements.

Now the induced function p¯:Bim(p)\overline{p}:B\to im(p) is surjective, and since im(p)im(p) is a subset of AA it is UU-small. Thus, by the “Collection” property of a universe, there exists a UU-small set CC, a surjection q:Cim(p)q:C\twoheadrightarrow im(p) and a function f:CBf:C\to B such that q=p¯fq = \overline{p} \circ f. We take B=CB'=C and the composite Cim(p)AC \to im(p)\to A as the function pp'; we claim that the composite relation MfM\circ f still satisfies (1) and (2) above. (We have not replaced YY yet, so this is still an intermediate step.) Property (1) follows since p(c)=p(f(c))p'(c) = p(f(c)) and (Mf) cM f(c)(M\circ f)_c \cong M_{f(c)}, while property (2) follows since im(p)=im(p)im(p) = im(p') by construction.

Now consider a tabulation BrZsYB' \overset{r}{\leftarrow} Z \overset{s}{\to} Y of MfM\circ f. Note that for any bBb\in B' we have r 1(b)(Mf) br^{-1}(b) \cong (M\circ f)_b, and therefore in particular r 1(b)r^{-1}(b) is UU-small by (1). Since BB' is also UU-small, the “Replacement” property of a universe implies that ZZ is also UU-small. But the family r o:BZr^o:B'\looparrowright Z is equivalent to MfM\circ f, in the sense that (r o) b(Mf) b(r^o)_b \cong (M\circ f)_b for all bBb\in B', so it also satisfies (1) and (2); thus we can take Y=ZY'=Z and M=r oM'=r^o.

Note that both the “Replacement” and “Collection” properties of a universe are required to show the SEAR Collection axiom for UU-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 UU-small if each of its fibers is. Note that then we can state the Replacement property as “the composite of UU-small functions is UU-small.” Now for functions g:CBg:C\to B and f:BAf:B\to A, the fiber of the dependent product Π fg\Pi_f g over aAa\in A is the subset of the function set ((fg) 1(a)) f 1(a)\Big((f g)^{-1}(a)\Big)^{f^{-1}(a)} consisting of functions s:f 1(a)(fg) 1(a)s: f^{-1}(a) \to (f g)^{-1}(a) such that gs=idg\circ s = \id. Thus, if ff and gg are UU-small, so is fgf g (by the “Replacement” property), and thus so is this fiber. Hence UU-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 f:BAf:B\to A. 1. ff is UU-small. 2. There exist a surjection p:CAp:C\to A and a function g:CUg:C\to U and two pullback squares

B q P k |E| f j A p C g U\array{B &\overset{q}{\leftarrow} & P & \overset{k}{\to} & {|E|}\\ ^f\downarrow && \downarrow^j && \downarrow\\ A &\underset{p}{\twoheadleftarrow} & C & \underset{g}{\to} & U}
  1. (If the axiom of choice holds) There exists a function g:AUg:A\to U and a pullback square
    B |E| f A g U\array{B & \overset{}{\to} & {|E|}\\ ^f\downarrow && \downarrow\\ A & \underset{g}{\to} & U}

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 pp has a section. Thus the difficulty is in showing that the first implies the second.

Suppose that f:BAf:B\to A is UU-small. This means that for any aAa\in A, there exists a uUu\in U and a bijection f 1(a)E uf^{-1}(a)\cong E_u. Let CC be the subset of A×U×P(B×|E|)A\times U\times P(B\times |E|) consisting of those triples (a,u,h)(a,u,h) such that hh is a bijection f 1(a)E uf^{-1}(a) \overset{\cong}{\to} E_{u}, and let p:CAp:C\to A and g:CUg:C\to U be the projections. Since ff is UU-small, pp is surjective. Define PP to be a pullback of ff along pp, with projections q:PBq:P\to B and j:PCj:P\to C, and define k:P|E|k:P\to {|E|} by (informally speaking) k(x)=h(q(x))k(x) = h(q(x)) where j(x)=(a,u,h)j(x) = (a,u,h). Since each hh is a bijection, kk makes PP a pullback of |E|{|E|}.

Last revised on February 27, 2017 at 21:44:03. See the history of this page for a list of all contributions to it.