#
Homotopy Type Theory
order > history (changes)

Showing changes from revision #3 to #4:
Added | ~~Removed~~ | ~~Chan~~ged

~~
~~

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

~~
~~## See also

~~
~~
Last revised on June 10, 2022 at 17:04:52.
See the history of this page for a list of all contributions to it.