Synthetic topos theory
[001J] Proposition

Let UU be a universe, let VV be a universe greater than or equal to UU, and let WW be a universe strictly greater than WW. Then the presheaves A(V),A(V):(Topos(1)(U))opW\mathbb {A}^{(V)},\mathbb {A}_{\bullet }^{(V)}:{(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U))}^{\mathord {\textnormal {\textsf {op}}}}\rightarrow W are sheaves.

Proof

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