Synthetic topos theory
[0003] Definition

Let \(U\) be a universe and let \(V\) be a universe strictly greater than \(U\). We define \(\mathord {\textnormal {\textsf {LexCocomp}}}(U,V)\) to be the locally full subcategory of the \(2\)-category of \(V\)-small categories whose objects are the \(V\)-small lex \(U\)-cocomplete categories and morphisms are the morphisms of lex \(U\)-cocomplete categories.