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)}\) is a \(\mathbb {I}\)-left fibration.