# Homotopy Type Theory order > history (Rev #3)

## Definition

A partial order $\leq$ over a type $A$ is an order (also called total order or linear order) if it comes with a family of dependent terms

$a:A, b:A \vdash \tau(a, b): \Vert R(a, b) + R(b, a) \Vert$

representing the totality condition for the partial order. $A$ is called an ordered type, totally ordered type, or linearly ordered type.