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$-universes 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:

*

*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.


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


*Is it true constructively that the poset of representable $\Sigma$-universes is directed? How about if I have a set-indexed family of representable $\Sigma$-universes – can I find another one containing them all?
 A: 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.


*

*$U$ contains an element $\ast$

*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).


*

*$\operatorname{Br}(\ast) = 1$

*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).


*

*If $u = \ast$, then $\operatorname{Br}(u)$ has one element, say $0$. Take $s(u, h)$ to be $h(0)$.

*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.
