Homotopy Type Theory
strict order > history (Rev #10, changes)
Showing changes from revision #9 to #10:
Added | Removed | Changed
<strict order
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 17, 2022 at 03:46:21 by
Anonymous?.
See the history of this page for a list of all contributions to it.