Showing changes from revision #9 to #10:
Added | Removed | Changed
A strict order (also called strict total order, strict linear order, or pseudo-order) on a type $A$ is a type family on $A \times A$ 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
$A$ is called a strictly ordered type.
Last revised on June 16, 2022 at 23:46:21. See the history of this page for a list of all contributions to it.