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

Showing changes from revision #2 to #3: Added | Removed | Changed

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

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

See also

• partial order

• strict order

• closed interval

• simplex category