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?
