Elementary theory of the category of sets

Definition

The Elementary Theory of the Category of Sets (ETCS) is the first-order theory of a category $\mathcal{S}$ with the following axioms.

1. $\mathcal{S}$ is an elementary topos.
2. $\mathcal{S}$ is nondegenerate: its terminal object $1$ is not an initial object.
3. $\mathcal{S}$ is well-pointed: for every two distinct morphisms $f, g \colon X \to Y$ there is a morphism $x \colon 1 \to X$ with $f \circ x \ne g \circ x$.
4. $\mathcal{S}$ has a natural numbers object $(N, z, s)$, as described below.
5. Every epimorphism $e \colon X \to Y$ in $\mathcal{S}$ has a section, a morphism $m \colon Y \to X$ with $e \circ m = \id_Y$.

A natural numbers object is an object $N$ with morphisms $z \colon 1 \to N$ and $s \colon N \to N$ with this property. For every object $X$ with morphisms $a \colon 1 \to X$ and $h \colon X \to X$ there is a unique $u \colon N \to X$ with $u \circ z = a$ and $u \circ s = h \circ u$.