Elementary Theory of the Category of Sets

In mathematics, the Elementary Theory of the Category of Sets or ETCS is a set of axioms for set theory proposed by William Lawvere in 1964.^[1] Although it was originally stated in the language of category theory, as Leinster pointed out, the axioms can be stated without references to category theory.

ETCS is a basic example of structural set theory, an approach to set theory that emphasizes sets as abstract structures (as opposed to collections of elements).

Axioms

The real message is this: simply by writing down a few mundane, uncontroversial statements about sets and functions, we arrive at an axiomatization that reflects how sets are used in everyday mathematics.

Tom Leinster, ^[2]

Informally, the axioms are as follows: (here, set, function and composition of functions are primitives)^[3]

1. Composition of functions is associative and has identities.
2. There is a set with exactly one element.
3. There is an empty set.
4. A function is determined by its effect on elements.
5. A Cartesian product exists for a pair of sets.
6. Given sets ${\displaystyle X}$ and ${\displaystyle Y}$, there is a set of all functions from ${\displaystyle X}$ to ${\displaystyle Y}$.
7. Given ${\displaystyle f:X\to Y}$ and an element ${\displaystyle y\in Y}$, the pre-image ${\displaystyle f^{-1}(y)}$ is defined.
8. The subsets of a set ${\displaystyle X}$ correspond to the functions ${\displaystyle X\to \{0,1\}}$.
9. The natural numbers form a set.
10. (weak axiom of choice) Every surjection has a right inverse (i.e., a section).

The resulting theory is weaker than ZFC. If the axiom schema of replacement is added as another axiom, the resulting theory is equivalent to ZFC.^[4]