basic constructions:
strong axioms
The Elementary Theory of the Category of Sets, ETCS for short, is a formulation of set-theoretic foundations in a category-theoretic spirit. As such, it is the prototypical structural set theory.
The axioms of ETCS can be summed up in one sentence as:
The category of sets is the topos which
is a well-pointed topos
has a natural numbers object
and satisfies the axiom of choice.
For more details see
Todd Trimble has a series of expositional writings on ETCS which provide a very careful introduction and at the same time a wealth of useful details.
Todd Trimble, ZFC and ETCS: Elementary Theory of the Category of Sets (nLab entry, original blog entry)
Todd Trimble, ETCS: Internalizing the logic (nLab entry, original blog entry)
Todd Trimble, ETCS: Building joins and coproducts (nLab entry, original blog entry)
ETCS was proposed by Bill Lawvere, who published an undergraduate set-theory textbook using it:
An informative discussion of the pros and cons of Lawvere’s approach can be found in
Erik Palmgren has a constructive predicative variant of ETCS, which can be summarized as: is a well-pointed -pretopos with a NNO and enough projectives (i.e. COSHEP is satisfied). Here “well-pointed” must be taken in its constructive sense, as including that the terminal object is indecomposable and projective.