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
representing the irreflexivity condition for the binary relation
a family of dependent terms
representing the comparison condition for the binary relation
a family of dependent terms
representing the connectedness condition for the binary relation
a family of dependent terms
representing the asymmetry condition for the binary relation
$A$ is called a strictly ordered type.