Synthetic topos theory
[0011] Proposition

Let \(U\) be a universe, let \(V\) be a universe strictly greater than \(U\), and let \(C\) be a \(V\)-small lex \(U\)-cocomplete category. Then the functor \(\mathord {\textnormal {\textsf {E}}}_{C}:{C}^{\mathord {\textnormal {\textsf {op}}}}\rightarrow \mathord {\textnormal {\textsf {LexCocomp}}}(U,V)\backslash C\) preserves \(U\)-small limits.

Proof

Observe that limits in \(\mathord {\textnormal {\textsf {LexCocomp}}}(U,V)\) are computed in the category of \(V\)-small categories. Then the claim is a consequence of descent.