Synthetic topos theory
[000Y] Proposition

Let \(U\) be a universe. Then the morphism \(\mathord {\textnormal {\textsf {p}}}:\mathbb {A}_{\bullet }\rightarrow \mathbb {A}\) in \(\mathord {\textnormal {\textsf {Topos}}}(U)\) is a left fibration.

Proof

By [000X].