Synthetic topos theory
[001J] Proposition

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 \(W\). Then the presheaves \(\mathbb {A}^{(V)},\mathbb {A}_{\bullet }^{(V)}:{(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U))}^{\mathord {\textnormal {\textsf {op}}}}\rightarrow W\) are sheaves.

Proof

\(\mathbb {A}^{(V)}\) is a sheaf by [001H]. \(\mathbb {A}_{\bullet }^{(V)}\) is a sheaf because coslicing commutes with limits.