# Homotopy Type Theory an axiomatization of the real numbers > history (Rev #4)

## Idea

I am going to define this in terms of Archimedean ordered Q-algebras…

## Definition

Strict order axioms: $\lt$

• For all terms $a:\mathbb{R}$, $a \lt a$ is false.

• For all terms $a:\mathbb{R}$, $b:\mathbb{R}$, $c:\mathbb{R}$, $a \lt c$ implies $a \lt b$ or $b \lt c$

• For all terms $a:\mathbb{R}$, $b:\mathbb{R}$, not $a \lt b$ and not $b \lt a$ implies $a = b$.

• For all terms $a:\mathbb{R}$, $b:\mathbb{R}$, $a \lt b$ implies not $b \lt a$

Archimedean property:

• For all terms $a:\mathbb{R}$, $b:\mathbb{R}$, and $c:\mathbb{R}$, $a \lt a + b$ and $a \lt a + c$ implies that there exists a natural number $n:\mathbb{N}$ such that $b \lt n c$, where $n c$ is the additive $n$-th power (n-fold addition)

One axioms: $1$

• $1 \lt 1 + 1$