Structure

Implication details

Claim: If a category has coproducts and is an elementary topos and has a generating collection and is locally essentially small, then it is a Grothendieck topos.

Proof: See Mac Lane–Moerdijk, Appendix, Prop. 4.4.

This implication has a dual.