Homotopy Type Theory order > history (Rev #3)


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 May 1, 2022 at 19:33:08 by Anonymous?. See the history of this page for a list of all contributions to it.