## 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 ## * [[ordered integral domain]] * [[Heyting field]] * [[Archimedean ordered field]]