[001J] -- 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.