Showing changes from revision #2 to #3: Added | Removed | Changed

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}$.

See also

• finite type
• decimal numeral representations of the natural numbers
• integers
• rational numbers
• decimal numbers
• real numbers

References

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)