Homotopy Type Theory decimal numbers > history (Rev #1)

Idea

The decimal numbers as familiar from school mathematics.

Definition

The type of decimal numbers, denoted $\mathbb{Z}[1/10]$, has several definitions as a higher inductive type.

Definition 1

Decimal numbers are defined as the higher inductive type generated by:

• A function $(-)/10^{(-)} : \mathbb{Z} \times \mathbb{N} \rightarrow \mathbb{Z}[1/10]$
• A dependent product of functions between identities representing that equivalent decimals are equal:
  $$equivdec : \prod_{a:\mathbb{Z}} \prod_{b:\mathbb{N}} \prod_{c:\mathbb{Z}} \prod_{d:\mathbb{N}} (a \cdot 10^d = c \cdot 10^b) \to (a/10^b = c/10^d)$$
• A set-truncator
  $$\tau_0: \prod_{a:\mathbb{Z}[1/10]} \prod_{b:\mathbb{Z}[1/10]} isProp(a=b)$$

Properties

TODO: Show that the decimal numbers are a Heyting ordered integral domain with decidable equality, decidable apartness, and decidable linear order, and that the decimal numbers are an integral subdomain of the rational numbers.

See also

• higher inductive type
• integers
• rational numbers