---
tag: B138JA6W20
kind: definition
name: Elementary theory of the category of sets
msc: [18B05, 03G30, 18A15]
defines: W448SK1RTY
uses: [A2DE66937D, 6837RS7N82, EK85VSSRMR, RVXDSY04KG, NKP5TPQ79X]
sources:
  - url: https://en.wikipedia.org/wiki/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|A2DE66937D]] $\mathcal{S}$ with the following axioms.

1. $\mathcal{S}$ is an elementary [[topos|6837RS7N82]].
2. $\mathcal{S}$ is nondegenerate: its [[terminal object|EK85VSSRMR]] $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|RVXDSY04KG]] $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$.

## Remarks

Example: the category $\mathbf{Set}$ of sets and functions, built in a model of ZFC, satisfies all five axioms.
Its natural numbers object is $\N$ with $0$ and $n \mapsto n + 1$, and the sections come from the axiom of choice.
Non-example: the category of sets with an action of the group $\Z/2$ is a nondegenerate topos with a natural numbers object, but it is not well-pointed.
Its terminal object is a one-point set, and a morphism $1 \to X$ is a fixed point of $X$.
On $X = \Z/2$ with the action by translation there are no fixed points, so the identity and the swap of $X$ are distinct but agree on all morphisms $1 \to X$.
In ETCS an element of $X$ is a morphism $1 \to X$, and the subsets of $X$ are classified by maps into the [[subobject classifier|NKP5TPQ79X]], which turns out to be $1 + 1$.
ETCS has no axiom schema of replacement.