Is every set smaller than a regular cardinal, constructively?

Constructively, my only interest in regular cardinals is in terms of the "$\Sigma$-universes" they generate. By a $\Sigma$-universe, I mean a collection of triples $(X,Y,f: X \to Y)$ closed under base change, composition, and isomorphism -- here $X,Y$ are sets and $f: X \to Y$ is a function between them. A $\Sigma$-universe can be viewed as a category where the morphisms are pullback squares. Let's say that a $\Sigma$-universe $U$ is essentially small or representable if, when viewed as a category in this way, it has a weakly terminal object.

In ZFC, representable $\Sigma$-universes are (almost) in bijection with regular cardinals. The bijection sends a regular cardinal $\kappa$ to the collection of functions with fibers of size $<\kappa$. The regularity of $\kappa$ corresponds to closure of the $\Sigma$-universe under composition.

Let's say

• there are enough representable $\Sigma$-unvierses if every function $f: X \to Y$ is contained in some representable $\Sigma$-universe.

In ZFC, there are enough representable $\Sigma$-universes because there are arbitrarily large regular cardinals.

Question:

1. Is it true constructively that there are enough representable $\Sigma$-universes? I assume this may depend on what one means by "constructively", but I don't know what the appropriate dividing lines might be.

2. If not, are there natural conditions on a constructive set theory that ensure the existence of enough representable $\Sigma$-universes?

3. Is it true constructively that the poset of representable $\Sigma$-universes is directed? How about if I have a set-indexed family of representble $\Sigma$-universes -- can I find another one containing them all?

• You might want to look for REA, the regular extension axiom, which is usually used within constructive Zermelo-Fraenkel CZF. See ncatlab.org/nlab/show/regular+extension+axiom and the references there, in particular the paper by M. Rathjen and B. Lubarsky. – godelian Jun 15 '18 at 21:25
• Gitik's model in which every uncountable cardinal is singular seems like it might be relevant. – Trevor Wilson Jun 15 '18 at 21:28
• What is a "base change"? Also, what is a function? In set theory, it would be a set of ordered pairs, but you may speak a different language. – Goldstern Jun 15 '18 at 21:38
• @Goldstern I don't intend anything exotic by "function" -- a function $f: X \to Y$ is the same thing as a subset $S \subseteq X \times Y$ such that $\forall x \in X \exists! y \in Y S(x,y)$. I'm sure there are subtleties about this that I don't have an appreciation of, so let me know if that's not sufficiently clear. Base change of $f: X \to Y$ along $g: Y' \to Y$ means the projection function $X \times_Y Y' \to Y'$. Here $X \times_Y Y' = \{(x,y) \in X \times Y' \mid f(x) = g(y)\}$. Here $g$ is an arbitrary function (not assumed to be in the $\Sigma$-universe). – Tim Campion Jun 15 '18 at 21:54
• Both of them use entire relations rather than functions -- maybe in a setting like a topos with some impredicativity one doesn't have to worry about this kind of thing? I should point out that this discussion also leads to a note by van den Berg where he shows (see the final remark) that in ZF, the axiom WISC implies there are arbitrarily large regular cardinals. (there's some discussion under the previous ncafe link too). I don't understand what's going on well enough to see if this generalizes. – Tim Campion Jun 16 '18 at 22:18

I think there are enough representable $\Sigma$-universes in any regular locally cartesian closed category with disjoint coproducts and $W$-types. One can show the category of sets has $W$-types in $\mathbf{ZF}$ and even $\mathbf{IZF}$. So I don't think any form of choice or existence of regular ordinal is necessary for this particular statement, although there are related statements that do require the existence of regular sets (I believe some of the results in algebraic set theory are like this). It's not provable in $\mathbf{CZF}$ that $\mathbf{Set}$ has $W$-types but it follows from axioms that are often added such as $\bigcup-\mathbf{REA}$ and holds in the type theory interpretation of set theory as long as the type theory has enough inductive types (if I recall correctly this means each universe of small types is closed under $W$-types).

Given $f : A \to B$, for each $b \in B$ we write $A_b$ for the fibre over $b$. We then define $U$ to be $W$-type defined as the smallest set closed under the following operations.

1. $U$ contains an element $\ast$
2. If $b \in B$ and $g : A_b \to U$, then $U$ contains an element $\sup(b, g)$.

We then define a function $\operatorname{Br}$ from $U$ to sets by recursion as follows. It's a little tricky to formalise this in a predicatively acceptable way, but I think this can be done using the notion of paths like in Theorem 2.1.5 in Benno van den Berg's thesis (essentially branches are maximal paths).

1. $\operatorname{Br}(\ast) = 1$
2. If $b \in B$ and $g : A_b \to U$, then $\operatorname{Br}(\sup(b, g)) = \Sigma_{a \in A_b} \operatorname{Br}(g(a))$

We can think of $W$-type as sets of well founded trees, and in this case $\operatorname{Br}(u)$ is the set of branches of the tree $u$. We then take the universe to be the projection $\pi_0 : \Sigma_{u \in U} \operatorname{Br}(u) \to U$.

Note that we can define a map $t : B \to U$ as follows. Given $b \in B$, define $t(b)$ to be $\sup(b, \lambda x.\ast)$. Then for each $b$, $\operatorname{Br}(t(b))$ is isomorphic to $A_b$, and so $f$ is a pullback of $\pi_0$ along $t$.

Next we show that if $u \in U$ and $h : \operatorname{Br}(u) \to U$, then we can define $s(u, h) \in U$ such that $\operatorname{Br}(s(u, h)) \cong \Sigma_{x \in \operatorname{Br}(u)} \operatorname{Br}(h(x))$. We do this by recursion (and check it works by induction).

1. If $u = \ast$, then $\operatorname{Br}(u)$ has one element, say $0$. Take $s(u, h)$ to be $h(0)$.
2. If $u = \sup(b, g)$, then for each $a \in A_b$, $h : \Sigma_{a \in A_b} \operatorname{Br}(g(a)) \to U$ restricts to a morphism $h_a : \operatorname{Br}(g(a)) \to U$. Take $s(u, h)$ to be $\sup(b, \lambda a.s(g(a), h_a))$.

(The way to visualise this is that are given a function from branches of a tree to trees, and we glue each tree to the end of its corresponding branch to get a bigger tree.)

We can now use this to show that pullbacks of $\pi_0 : \Sigma_{u \in U} \operatorname{Br}(u) \to U$ are closed under composition. Every pullback is isomorphic to one where the codomain is an object $Y$, the bottom of the pullback is a map $t : Y \to U$ and the map is the projection $\Sigma_{y \in Y} \operatorname{Br}(t(y)) \to Y$. If we are given two composable maps $X \to Y$ and $Y \to Z$ that are both pullbacks of $\pi_0$, say along $t : Z \to U$ and $r : Y \to U$, then the maps are isomorphic to ones where $Y = \Sigma_{z \in Z} \operatorname{Br}(t(z))$ and $X = \Sigma_{z \in Z} \Sigma_{w \in \operatorname{Br}(t(z))} \operatorname{Br}(r(z, w))$. We can then use the map $s$ constructed above to witness the composition as a pullback of $\pi_0$. Namely, for each $z \in Z$, $r$ restricts to a map $r_z : \operatorname{Br}(t(z)) \to U$. We can then take $t' : Z \to U$ to be $t'(z) := s(t(z), r_z)$. The composition is then the pullback along $t'$.

I think the other two parts follow from the existence of enough representable $\Sigma$-universes. Because if we have a family of universes, we can take the coproduct of all the universes in the family and then construct a universe for that.

• van den Berg's note showing how to do this in ZF was certainly suggestive that some W-type construction could work, but since he was interested in WISC in the note, it left the impression that something like WISC might also be necessary. So to see that it can be done with just W-types is fantastic. Thanks! It's also amazing to see that the statement as I formulated it is true in ZF even though there may not be enough regular cardinals in the ordinary sense! I suppose what must happen is that in the representation $B\to U$ constructed, not every smaller subset of $U$ appears as a fiber. – Tim Campion Jun 19 '18 at 14:14
• I was thinking of adding a "descent" condition saying that if $Y\times_X X' \to X'$ is in the universe for some surjection $X' \to X$, then $Y \to X$ is in the universe. I suppose in order to get enough representable $\Sigma$-universes satisfying this condition, perhaps something like WISC might be necessary. – Tim Campion Jun 19 '18 at 14:40
• That would definitely prevent the construction I gave from working. You can see e.g. Van den Berg, Moerdijk, Aspects of Predicative Algebraic Set Theory I, for a typical approach to this kind of thing and they include that descent condition in Proposition 2.10. They also use a weaker notion of representability that I think avoids some of these issues. – aws Jun 19 '18 at 15:07