Homotopy Type Theory
strict order > history (Rev #2)
Definition
A binary relation over a type is a strict order (also called strict total order, strict linear order, or pseudo-order) if it comes with
-
a family of dependent terms
representing the irreflexivity condition for the binary relation
-
a family of dependent terms
representing the comparison condition for the binary relation
-
a family of dependent terms
representing the connectedness condition for the binary relation
-
a family of dependent terms
representing the asymmetry condition for the binary relation
is called a strictly ordered type.
See also
Revision on March 12, 2022 at 03:29:14 by
Anonymous?.
See the history of this page for a list of all contributions to it.