Synthetic topos theory
[0019] Definition

Let \(U\) be a universe and let \(V\) be a universe strictly greater than \(U\). We define \(\mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),V)\) to be the full subcategory of \(\mathord {\textnormal {\textsf {Fun}}}({(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U))}^{\mathord {\textnormal {\textsf {op}}}},V)\) spanned by the sheaves in the sense of [0016].