Synthetic topos theory
[000N] Definition

Let \(U\) be a universe. We say a morphism \(f:Y\rightarrow X\) in \(\mathord {\textnormal {\textsf {Topos}}}(U)\) is étale if there exists a (necessarily unique by [000M]) pullback square from \(f\) to \(\mathord {\textnormal {\textsf {p}}}:\mathbb {A}_{\bullet }\rightarrow \mathbb {A}\).