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.

5more comments