Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
A comparison or cotransitive relation or weakly linear relation on a set is a (binary) relation on such that in every pair of related elements, any other element is related to one of the original elements in the same order as the original pair:
which generalises from to any (finite, positive) number of elements. To include the case where , we must explicitly state that the relation is irreflexive.
Alternatively, this is the same condition as
Comparisons are most often studied in constructive mathematics. In particular, the relation on the (located Dedekind) real numbers is an irreflexive comparison, even though its negation is not constructively total. (Indeed, is a pseudo-order, even though is not constructively a total order.)
A comparison is a cartesian monoidal semicategory enriched on the co-Heyting algebra , where is the Heyting algebra of truth values.
In dependent type theory, there are two different notions of a cotransitive or weakly linear relation
This distinction could also be made in set theory: Given a proposition , can be made into a subsingleton set by considering the subset of the singleton . Let denote the support of the set , and let denote the disjoint union of sets and . Then
Wikipedia, Apartness relation
Wikipedia, Pseudo-order
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Auke Booij, Analysis in univalent type theory (2020) etheses:10411, pdf
Last revised on September 25, 2024 at 22:24:36. See the history of this page for a list of all contributions to it.