# Homotopy Type Theory ordered field > history (changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

## Definition

### With strict order

An ordered field is a strictly ordered integral $\mathbb{Q}$-algebra such that for every element $a:A$ such that $\max(a, -a) \gt 0$, there is an element $b:A$ such that $a \cdot b = 1$.

### With positivity

An ordered field is a commutative ring with a predicate $\mathrm{isPositive}$ such that

• zero is not positive:
$\mathrm{isPositive}(0) \to \emptyset$
• one is positive:
$\mathrm{isPositive}(1)$
• for every term $a:A$, if $a$ is not positive and $-a$ is not positive, then $a = 0$
$\prod_{a:A} ((\mathrm{isPositive}(a) \to \emptyset) \times (\mathrm{isPositive}(-a) \to \emptyset)) \to (a = 0)$
• for every term $a:A$, if $a$ is positive, then $-a$ is not positive.
$\prod_{a:A} \prod_{b:A} \mathrm{isPositive}(a) \to (\mathrm{isPositive}(-a) \to \emptyset)$
• for every term $a:A$, $b:A$, if $a$ is positive, then either $b$ is positive or $a - b$ is positive.
$\prod_{a:A} \prod_{b:A} \mathrm{isPositive}(a) \to \left[\mathrm{isPositive}(b) + \mathrm{isPositive}(a - b)\right]$
• for every term $a:A$, $b:A$, if $a$ is positive and $b$ is positive, then $a + b$ is positive
$\prod_{a:A} \prod_{b:A} \mathrm{isPositive}(a) \times \mathrm{isPositive}(b) \to \mathrm{isPositive}(a + b)$
• for every term $a:A$, $b:A$, if $a$ is positive and $b$ is positive, then $a \cdot b$ is positive
$\prod_{a:A} \prod_{b:A} \mathrm{isPositive}(a) \times \mathrm{isPositive}(b) \to \mathrm{isPositive}(a \cdot b)$
• for every term $a:A$, if $a$ is positive, then there exists a $b$ such that $a \cdot b = 1$ and $b \cdot a = 1$
$\prod_{a:A} \mathrm{isPositive}(a) \to \left[\sum_{b:A} (a \cdot b = 1) \times (b \cdot a = 1)\right]$