[[!redirects whole numbers]] #Contents# * table of contents {:toc} ## Idea ## The natural numbers as familiar from school mathematics. ## Definitions ## The type of __natural numbers__, denoted $\mathbb{N}$ and also called __whole numbers__, is inductively generated by a term $z:\mathbb{N}$ and an endofunction $s:\mathbb{N} \to \mathbb{N}$. ## See also ## * [[decimal numeral representations of the natural numbers]] * [[integers]] * [[rational numbers]] * [[decimal numbers]] * [[real numbers]] ## References ## [[HoTT book]]