Homotopy Type Theory ordered integral domain > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Definition

With strict order

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

With positivity

An ordered integral domain is a Heyting integral domain with a predicate $\mathrm{isPositive}$ such that

• zero is not positive:

• one is positive:

• for every term $a:A$, if $a$ is not positive and $-a$ is not positive, then $a = 0$

• for every term $a:A$, if $a$ is positive, then $-a$ is not positive.

• for every term $a:A$, $b:A$, if $a$ is positive, then either $b$ is positive or $a - b$ is positive.

• for every term $a:A$, $b:A$, if $a$ is positive and $b$ is positive, then $a + b$ is positive

• for every term $a:A$, $b:A$, if $a$ is positive and $b$ is positive, then $a \cdot b$ is positive

Examples

• The integers are an ordered integral domain.

• The rational numbers are a ordered integral domain

• Every ordered field is a ordered integral domain.

See also

• Heyting integral domain

• ordered field

• unit interval

• Archimedean ordered integral domain