Synthetic topos theory
[000W] Definition

Let \(U\) be a universe and let \(X\) be a \(U\)-topos. We define \(\mathord {\textnormal {\textsf {Etale}}}(X)\) to be the full subcategory of \(\mathord {\textnormal {\textsf {Topos}}}(U)/X\) spanned by the étale morphisms with codomain \(X\).