Homotopy Type Theory order > history (changes)

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


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

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