Is there an axiomatisation of some kind of category theory and a definition of sets in this framework such that the axioms of ZF resp. ZFC are theorems?

4$\begingroup$ If you formulate everything correctly, ECTS + separation is equivalent to ZFC. There is a translation you need to do because ECTS is twosorted. See Tom Leinster's nice summary article: arxiv.org/abs/1212.6543 $\endgroup$ – Harry Gindi Jan 20 at 12:33

$\begingroup$ Thanks for the reference. $\endgroup$ – Jörg Neunhäuserer Jan 20 at 12:48

1$\begingroup$ I think I meant replacement, not separation. It's whatever Leinster calls axiom 11. $\endgroup$ – Harry Gindi Jan 20 at 13:19
Yes, this is a wellknown fact that goes back to Cole, Mitchell, and Osius in the 70's. The relevant kind of category is, as Harry says in the comments, a wellpointed topos with extra properties; Lawvere's Elementary Theory of the Category of Sets is an axiomatization of such a category. To define ZFsets in such a category you build them along with their hereditary membership structure as wellfounded graphs; there is a good introduction in Chapter VI of Mac Lane & Moerdijk's book Sheaves in Geometry and Logic. If you want a very detailed treatment that includes analogous results for a wide variety of set theories including both ZF and ZFC and also weaker and constructive versions, there is my own paper Comparing material and structural set theories.

$\begingroup$ You linked the v2 not the v3 of your paper. Was that intentional $\endgroup$ – Harry Gindi Jan 20 at 15:35


2$\begingroup$ @HarryGindi Yes, the two versions are identical, but v2 has the more permissive license. (:O $\endgroup$ – Mike Shulman Jan 20 at 16:53