Homotopy Type Theory
ordered abelian group > history (changes)
Showing changes from revision #5 to #6:
Added | Removed | Changed
Definition
With strict order
An ordered abelian group is an abelian group $A$ with a strict order $\lt$ and a family of dependent terms
$a:A, b:A \vdash \alpha(a, b): (0 \lt a) \times (0 \lt b) \to (0 \lt a + b)$
With positivity
An ordered abelian group is an abelian group $A$ with a predicate $\mathrm{isPositive}$ such that
$\mathrm{isPositive}(0) \to \emptyset$
- 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)$
Examples
See also
Last revised on June 16, 2022 at 22:40:15.
See the history of this page for a list of all contributions to it.