Whenever editing is allowed on the nLab again, this article should be ported over there.

A decimal number algebra homomorphism between two decimal number algebras $A$ and $B$ is a function $f \in B^A$ such that

The category of decimal number algebras is the category $DNA$ whose objects $Ob(DFA)$ are decimal number algebras and whose morphisms $Mor(DNA)$ are decimal numbers algebra homomorphisms. The set of decimal numbers, denoted $\mathbb{Z}[1/10]$, is defined as the initial object in the category of decimal number algebras.

In homotopy type theory

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)$$

Mathematical structures on the decimal numbers

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

Sign

Positive sign

We define the dependent type is positive, denoted as $isPositive(a/10^b)$, to be the following:

for $a:\mathbb{Z}$, $b:\mathbb{N}$, dependent types $m\gt n$ indexed by $m, n:\mathbb{Z}$.

Negative sign

We define the dependent type is negative, denoted as $isNegative(a/10^b)$, to be the following:

for $a:\mathbb{Z}$, $b:\mathbb{N}$, dependent types $m\gt n$ indexed by $m, n:\mathbb{Z}$.

Zero sign

We define the dependent type is zero, denoted as $isZero(a/10^b)$, to be the following:

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

Non-positive sign

We define the dependent type is non-positive, denoted as $isNonPositive(a/10^b)$, to be the following:

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

Non-negative sign

We define the dependent type is non-negative, denoted as $isNonNegative(a/10^b)$, to be the following:

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

Non-zero sign

We define the dependent type is non-zero, denoted as $isNonZero(a/10^b)$, to be the following:

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

Order structure on the decimal numbers

Less than

We define the dependent type is less than, denoted as $a/10^b \lt c/10^d$, to be the following:

$a/10^b \lt c/10^d \coloneqq isPositive(c/10^d - a/10^b)$

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

Greater than

We define the dependent type is greater than, denoted as $a/10^b \gt c/10^d$, to be the following:

$a/10^b \gt c/10^d \coloneqq isNegative(c/10^d - a/10^b)$

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

Apart from

We define the dependent type is apart from, denoted as $a/10^b # c/10^d$, to be the following:

$a/10^b # c/10^d \coloneqq isNonZero(c/10^d - a/10^b)$

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

Less than or equal to

We define the dependent type is less than or equal to, denoted as $a/10^b \leq c/10^d$, to be the following:

$a/10^b \lt c/10^d \coloneqq isNonNegative(c/10^d - a/10^b)$

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

Greater than or equal to

We define the dependent type is greater than or equal to, denoted as $a/10^b \geq c/10^d$, to be the following:

$a/10^b \geq c/10^d \coloneqq isNonPositive(c/10^d - a/10^b)$

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

Pseudolattice structure on the decimal numbers

Ramp

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

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

Minimum

We define the minimum $min:\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}$.

Maximum

We define the maximum $max:\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}$.

Absolute value

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

for $a:\mathbb{Z}$, $b:\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.