# Homotopy Type Theory strict order > history (Rev #5)

## 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.