Synthetic topos theory
[000E] Definition

Let \(U\) be a universe and let \(C\) and \(D\) be lex \(U\)-cocomplete universes. We define \(\mathord {\textnormal {\textsf {LexCocomp}}}_{U}(C,D)\) to be the full subcategory of the category of functors from \(C\) to \(D\) spanned by the morphisms of lex \(U\)-cocomplete categories.