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

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

Definition

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

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

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

See also

Revision on March 12, 2022 at 03:17:07 by Anonymous?. See the history of this page for a list of all contributions to it.