A strict order (also called strict total order, strict linear order, or pseudo-order) on a type $A$ is a type family on $A \times A$ with
a family of dependent terms
representing that the dependent type is a proposition
a family of dependent terms
representing the irreflexivity condition for the dependent type
a family of dependent terms
representing the comparison condition for the dependent type
a family of dependent terms
representing the connectedness condition for the dependent type
a family of dependent terms
representing the asymmetry condition for the dependent type
$A$ is called a strictly ordered type.