Synthetic topos theory
[001I] 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\). We define presheaves

\(\mathbb {A}^{(V)},\mathbb {A}_{\bullet }^{(V)}:{(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U))}^{\mathord {\textnormal {\textsf {op}}}}\rightarrow W\)
by
\(\mathbb {A}^{(V)}(X)=\mathord {\textnormal {\textsf {Obj}}}(\mathop {\Uparrow ^{V}}(\mathord {\textnormal {\textsf {Sh}}}(X)))\) and \(\mathbb {A}_{\bullet }^{(V)}(X)=\mathord {\textnormal {\textsf {Obj}}}(\mathop {\Uparrow ^{V}}(\mathord {\textnormal {\textsf {Sh}}}(X))\backslash \mathord {\textnormal {\textsf {1}}})\).
We also define a morphism \(\mathord {\textnormal {\textsf {p}}}^{(V)}:\mathbb {A}_{\bullet }^{(V)}\rightarrow \mathbb {A}^{(V)}\) by the codomain projection.