Natural set construction with Elementary Theory of the Category of Sets

Question

I'm learning type theory by myself, so first I'm trying to understand the differences between ZFC and ETCS. I'm familiar with ZFC, it is how I reason about sets, but I'm having trouble trying to see things through the ETCS. I stumbled across the definition of the natural set. ZFC looks very straight-forward but ETCS looks like I'm missing something. The definition I found is $\Bbb{N}$ as having an element 0 and a function $$ s: \Bbb{N} →\Bbb{N} $$ It is trivial that $s$ has closure, but it means nothing else to me. How exactly $s$ relates to 0? Is that definition loose and lacking things or I'm just missing the point of Elementary Theory of the Category of Sets?

Answer 1

What you're missing is the universal property: that $1 \xrightarrow{0} \mathbb{N} \xrightarrow{s} \mathbb{N}$ is initial among such diagrams. Given any other diagram

$$ 1 \xrightarrow{a} X \xrightarrow{r} X $$

there is a unique map $f : \mathbb{N} \to X$ such that $f0 = a$ and $fs = rf$.

That this map exists and is unique is basically the principle of recursive definition, where $a$ is the initial value and $r$ is the recursive step. For example, you can see that this implies the iterates

$$ f0 = a \qquad fs0 = ra \qquad fss0 = rra \qquad fsss0 = rrra $$