Synthetic topos theory
[000S] Proposition

Let \(U\) be a universe. Then étale morphisms in \(\mathord {\textnormal {\textsf {Topos}}}(U)\) are closed under pullback.

Proof

This is by definition.