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\). Then the morphism \(\mathord {\textnormal {\textsf {p}}}^{(V)}:\mathbb {A}_{\bullet }^{(V)}\rightarrow \mathbb {A}^{(V)}\) in \(\mathord {\textnormal {\textsf {Sh}}}(\mathord {\textnormal {\textsf {Topos}}}^{(1)}(U),W)\) is univalent.