Synthetic topos theory
[0004] Definition

Let \(U\) be a universe. The \(2\)-category \(\mathord {\textnormal {\textsf {Logos}}}(U)\) of \(U\)-logoses is defined to be the smallest full subcategory of \(\mathord {\textnormal {\textsf {LexCocomp}}}(U,V)\) spanned by the \(U\)-compact objects, where \(V\) is some universe strictly greater than \(U\). Note that the choice of \(V\) does not matter.