Let \(U\) be a universe. Then the morphism \(\mathord {\textnormal {\textsf {p}}}:\mathbb {A}_{\bullet }\rightarrow \mathbb {A}\) in \(\mathord {\textnormal {\textsf {Topos}}}(U)\) satisfies directed univalence. That is, for any object \(X:\mathord {\textnormal {\textsf {Topos}}}(U)\), the functor

\(\mathord {\textnormal {\textsf {Hom}}}_{\mathord {\textnormal {\textsf {Topos}}}(U)}(X,\mathbb {A})\rightarrow \mathord {\textnormal {\textsf {Topos}}}(U)/X\) defined by the pullback of the left fibration \(\mathord {\textnormal {\textsf {p}}}:\mathbb {A}_{\bullet }\rightarrow \mathbb {A}\) is fully faithful.