[[!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}$. ### Division and remainder ### Given a natural number $n$, we define the division function $m \div n: \mathbb{N} \times \mathbb{N}_{+} \to \mathbb{N}$ with terms $$p:\prod_{m:\mathbb{N}} \prod_{n:\mathbb{N}_{+}} (m \leq n) \to (m \div n = 0)$$ $$q:\prod_{m:\mathbb{N}} \prod_{n:\mathbb{N}_{+}} ((m + n) \div n = 1 + m \div n)$$ and the remainder function $$m\ \%\ n \coloneqq m - (m \div n) \cdot n$$ ## See also ## * [[finite type]] * [[decimal numeral representations of the natural numbers]] * [[infinite decimal representation of a unit interval]] * [[integers]] * [[rational numbers]] * [[decimal numbers]] * [[real numbers]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) category: not redirected to nlab yet