Synthetic topos theory
[001F] Exercise

Let \(U\) be a universe and let \(V\) be a universe greater than or equal to \(U\). For any \(U\)-logos \(C\), the unit \(C\rightarrow \mathop {\Uparrow ^{V}}C\), which is a morphism in \(\mathord {\textnormal {\textsf {LexCocomp}}}(U,W)\) for some universe \(W\) strictly greater than \(V\), is fully faithful. We thus regard \(C\) as a full subcategory of \(\mathop {\Uparrow ^{V}}C\).