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

## Definition

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

$a:A, b:A \vdash \pi(a, b): \prod_{c:(a \lt b)} \prod_{d:(a \lt b)} c = d$

representing that the dependent type is a proposition

• a family of dependent terms

$a:A \vdash \iota(a): (a \lt a) \to \emptyset$

representing the irreflexivity condition for the dependent type

• 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 dependent type

• 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 dependent type

• 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 dependent type

$A$ is called a strictly ordered type.