CatDat

Implication Details

Claim: If a category has a strict terminal object, then it has a natural numbers object.

Proof: Let $1$ be a strict terminal object. For every endomorphism $g : X \to X$ and every morphism $a : 1 \to X$, we have $g \circ a = a$, because $a$ is an isomorphism and hence $X$ is terminal, which forces $g = \id_X$. Therefore, $(1,\id_1,\id_1)$ is a natural numbers object by Lemma 3 here.