Synthetic topos theory
[001E] Definition

Let \(U\) be a universe, let \(V\) be a universe greater than or equal to \(U\), and let \(W\) be a universe strictly greater than \(V\). The forgetful functor \(\mathord {\textnormal {\textsf {LexCocomp}}}(V,W)\rightarrow \mathord {\textnormal {\textsf {LexCocomp}}}(U,W)\) has a left adjoint. This left adjoint takes \(U\)-compact objects in \(\mathord {\textnormal {\textsf {LexCocomp}}}(U,W)\) to \(V\)-compact objects in \(\mathord {\textnormal {\textsf {LexCocomp}}}(V,W)\) and thus induces a functor \(C\mapsto \mathop {\Uparrow ^{V}}C:\mathord {\textnormal {\textsf {Logos}}}(U)\rightarrow \mathord {\textnormal {\textsf {Logos}}}(V)\). For a \(U\)-logos \(C\), the \(V\)-logos \(\mathop {\Uparrow ^{V}}C\) is called the \(V\)-enlargement of \(C\). Notice that the choice of \(W\) does not matter.