Synthetic topos theory
[0007] Lemma

Let \(U\) be a universe and let \(V\) be a universe strictly greater than \(U\). Then \(\mathord {\textnormal {\textsf {Logos}}}(U)\) is closed in \(\mathord {\textnormal {\textsf {LexCocomp}}}(U,V)\) under \(U\)-small colimits.

Proof

This is because \(U\)-compact objects in a \((V,U)\)-presentable category are closed under \(U\)-small colimits.