Homotopy Type Theory ordered field > history (Rev #1)

Definition

An ordered field is a Heyting field $(A, +, -, 0, \cdot, 1, #)$ with

a strict order $\lt$
a term $s:0 \lt 1$
two families of dependent terms

a:A, b:A \vdash \alpha(a, b): (0 \lt a) \times (0 \lt b) \to (0 \lt a + b)

a:A, b:A \vdash \mu(a, b): (0 \lt a) \times (0 \lt b) \to (0 \lt a \cdot b)

Examples

The rational numbers are a ordered field.

See also

Revision on March 12, 2022 at 03:55:40 by Anonymous?. See the history of this page for a list of all contributions to it.