Proposition C.5

For every small category $J$ whose object type lies in universe $u$, assume that its object type is at most countable and that the type of all triples $(i,j,\alpha)$, with $i,j$ objects and $\alpha:i\to j$ a morphism, is at most countable. Let $F:J\to\mathrm{TopCat}_u$ be any functor to topological spaces with underlying types in universe $u$. Suppose that for every object $j$, there exist an at most countable index type $I_j$ in universe $u$, compact Hausdorff spaces $K_{j,i}$ in universe $u$, and continuous maps $f_{j,i}:K_{j,i}\to F(j)$ whose images cover $F(j)$, such that a subset $A\subseteq F(j)$ is open if and only if every $f_{j,i}^{-1}(A)$ is open. Then the colimit $C=\operatorname{colim}F$, taken in the category of topological spaces, admits an at most countable index type $L$ in universe $u$, compact Hausdorff spaces $H_\ell$ in universe $u$, and continuous maps $h_\ell:H_\ell\to C$ whose images cover $C$, such that a subset $B\subseteq C$ is open if and only if every $h_\ell^{-1}(B)$ is open. The category $J$ may be empty, in which case the hypothesis on its objects is vacuous and its colimit is the empty space; all the countable index types and compact Hausdorff spaces may also be empty.