Idea

The decimal numbers as familiar from school mathematics.

Contents

Definition

The type of decimal numbers, denoted $\mathbb{Z}[1/10]$, is defined as the higher inductive type generated by:

• A function $(-)/10^{(-)}:\mathbb{Z} \times \mathbb{N} \rightarrow \mathbb{Z}[1/10]$. The integer $a:\mathbb{Z}$ represents the integer if one ignores the decimal separator in the decimal numeral representation of the decimal number, and the natural number $b:\mathbb{N}$ represents the number of digits to the left of the final digit where the decimal separator ought to be placed after in the decimal numeral representation of the decimal number.
• 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)$$

  (i.e. 1.00 = 1.000 with decimal numeral representations)

• A set-truncator
  $$\tau_0: \prod_{a:\mathbb{Z}[1/10]} \prod_{b:\mathbb{Z}[1/10]} isProp(a=b)$$

Raw ring structure on the decimal numbers

Zero

We define zero $0:\mathbb{Z}[1/10]$ to be the following:

Addition

We define addition $(-)+(-):\mathbb{Z}[1/10] \times \mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ to be the following:

for $a:\mathbb{Z}$, $b:\mathbb{N}$, $c:\mathbb{Z}$, $d:\mathbb{N}$.

Negation

We define negation $-(-):\mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ to be the following:

for $a:\mathbb{Z}$, $b:\mathbb{N}$.

Subtraction

We define subtraction $(-)-(-):\mathbb{Z}[1/10] \times \mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ to be the following:

for $a:\mathbb{Z}$, $b:\mathbb{N}$, $c:\mathbb{Z}$, $d:\mathbb{N}$.

One

We define one $1:\mathbb{Z}[1/10]$ to be the following:

Multiplication

We define multiplication $(-)\cdot(-):\mathbb{Z}[1/10] \times \mathbb{Z}[1/10] \to \mathbb{Z}[1/10]$ to be the following:

for $a:\mathbb{Z}$, $b:\mathbb{N}$, $c:\mathbb{Z}$, $d:\mathbb{N}$.

Exponentiation

We define exponentiation $(-)^{(-)}:\mathbb{Z}[1/10] \times \mathbb{N} \to \mathbb{Z}[1/10]$ to be the following:

for $a:\mathbb{Z}$, $b:\mathbb{N}$, $n:\mathbb{N}$.

Properties

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

10 is a unit term.

Thus this is true:

this forms the basis of scientific notation.

See also

• higher inductive type
• integers
• rational numbers