[[!redirects pseudo-order]] [[!redirects strict total order]] [[!redirects strict linear order]] [[!redirects strictly ordered type]] ## Definition ## A [[binary relation]] $\lt$ over a type $A$ is a __strict order__ (also called __strict total order__, __strict linear order__, or __pseudo-order__) if it comes with * a family of dependent terms $$a:A \vdash \iota(a): (a \lt a) \to \emptyset$$ representing the irreflexivity condition for the binary relation * a family of dependent terms $$a:A, b:A, c:A \vdash \kappa(a): (a \lt c) \to \left[(a \lt b) + (b \lt c) \right]$$ representing the comparison condition for the binary relation * a family of dependent terms $$a:A, b:A \vdash \gamma(a): ((a \lt b) \to \emptyset) \times ((b \lt a) \to \emptyset) \to (a = b)$$ representing the connectedness condition for the binary relation * a family of dependent terms $$a:A, b:A \vdash \alpha(a, b): (a \lt b) \to ((b \lt a) \to \emptyset)$$ representing the asymmetry condition for the binary relation $A$ is called a __strictly ordered type__. ## See also ## * [[binary relation]] * [[dense strict order]] * [[ordered integral domain]]