Synthetic topos theory
[0012] Proposition

Let \(U\) be a universe and let \(X\) be a \(U\)-topos. Then the functor \(\mathord {\textnormal {\textsf {E}}}_{\mathord {\textnormal {\textsf {Sh}}}(X)}:{(\mathord {\textnormal {\textsf {Sh}}}(X))}^{\mathord {\textnormal {\textsf {op}}}}\rightarrow \mathord {\textnormal {\textsf {Logos}}}(U)\backslash \mathord {\textnormal {\textsf {Sh}}}(X)\) restricts to an equivalence \(\mathord {\textnormal {\textsf {Sh}}}(X)\simeq \mathord {\textnormal {\textsf {Etale}}}(X)\).

Proof

By definition.