Contents

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

and the remainder function

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, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)