Implication details

Proof: Let $1$ be a terminal object and consider the copower $$\textstyle N \coloneqq \coprod_{n \in \IN} 1$$ with inclusions $i_n : 1 \to N$ for $n \in \IN$. Define $z \coloneqq i_0 : 1 \to N$ and $s : N \to N$ by $$s \circ i_n \coloneqq i_{n+1},$$ using the universal property of the copower. Given a morphism $a : 1 \to X$ and a morphism $g : X \to X$, recursively define morphisms $\phi_n : 1 \to X$ by $\phi_0 \coloneqq a$ and $\phi_{n+1} \coloneqq g \circ \phi_n$. (Here we are essentially using the fact that $(\IN,0,n \mapsto n+1)$ is a natural numbers object in $\Set$.) The universal property of the copower gives a unique morphism $\Phi : N \to X$ satisfying $\Phi \circ i_n = \phi_n$. In particular, $\Phi \circ z = \phi_0 = a$. Moreover, $\Phi \circ s = g \circ \Phi$, since for every $n \in \IN$ we have $$\Phi \circ s \circ i_n = \Phi \circ i_{n+1} = \phi_{n+1} = g \circ \phi_n = g \circ \Phi \circ i_n.$$ Conversely, suppose that $\Phi' : N \to X$ satisfies $\Phi' \circ z = a$ and $\Phi' \circ s = g \circ \Phi'$. Then $$\Phi' \circ i_n = \Phi \circ i_n$$ follows by induction on $n \in \IN$. It holds for $n=0$ since both sides are $a : 1 \to X$. If it holds for $n$, then $$\begin{align*} \Phi' \circ i_{n+1} & = \Phi' \circ s \circ i_n \\ & = g \circ \Phi' \circ i_n \\ & = g \circ \Phi \circ i_n \\ & = \Phi \circ s \circ i_n \\ & = \Phi \circ i_{n+1}. \end{align*}$$ Since $\Phi' \circ i_n = \Phi \circ i_n$ for every $n \in \IN$, we conclude that $\Phi' = \Phi$.