Set, Category, Topos

ETCS#

A good exposition Tom Leinster, Rethinking set theory.pdf

Indeed, ETCS says exactly that sets and functions form a topos of a special sort: a ‘well-pointed topos with natu- ral numbers object and choice’. So a topos is not only a generalized space; it is also a generalized universe of sets.

The strength of ETCS is slightly weaker than ZFC. It corresponds to the fragment of ZFC: Zermelo with bounded comprehension and choice. Adding an eleventh axiomm scheme, “replacement”, we then get a system bi-interpretable with ZFC. Definaility.