Natural Number

The natural numbers, $\mathbb{N}$ can be defined as an Initial Algebra of the following functor:

$$X\Rightarrow 1+X$$

Then $\mathrm{zero}=\mathrm{inl}\ast$, and $\mathrm{suc}x=\mathrm{inr}x$.

Alternatively $\mathbb{N}$ can be defined in Agda,

$$\begin{array}{rl}& \mathrm{data}\mathbb{N}:\mathrm{Set}\mathrm{where}\\ & \mathrm{zero}:\mathbb{N}\\ & \mathrm{suc}:\mathbb{N}\to \mathbb{N}\end{array}$$