## Definition ## An __ordered integral domain__ is a [[Heyting integral domain]] $(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 [[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]]