Homotopy Type Theory
strict order > history (Rev #9)
Definition
A strict order (also called strict total order, strict linear order, or pseudo-order) on a type is a type family on with
-
a family of dependent terms
representing that the dependent type is a proposition
-
a family of dependent terms
representing the irreflexivity condition for the dependent type
-
a family of dependent terms
representing the comparison condition for the dependent type
-
a family of dependent terms
representing the connectedness condition for the dependent type
-
a family of dependent terms
representing the asymmetry condition for the dependent type
is called a strictly ordered type.
See also
Revision on June 16, 2022 at 02:56:48 by
Anonymous?.
See the history of this page for a list of all contributions to it.