nLab comparison

Redirected from "purely cotransitive".

Contents

 Definition

A comparison or cotransitive relation or weakly linear relation on a set AA is a (binary) relation \sim on AA 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:

(x,y,z:A),xzxyyz\forall (x, y, z: A),\; x \sim z \;\Rightarrow\; x \sim y \;\vee\; y \sim z

which generalises from 33 to any (finite, positive) number of elements. To include the case where n=1n = 1, we must explicitly state that the relation is irreflexive.

Alternatively, this is the same condition as

(x,z:A),xz(y:A),xyyz\forall (x, z: A),\; x \sim z \;\Rightarrow\; \forall (y: A),\; x \sim y \;\vee\; y \sim z

Comparisons are most often studied in constructive mathematics. In particular, the relation <\lt on the (located Dedekind) real numbers is an irreflexive comparison, even though its negation \geq is not constructively total. (Indeed, <\lt is a pseudo-order, even though \geq is not constructively a total order.)

A comparison is a cartesian monoidal semicategory enriched on the co-Heyting algebra TV opTV^\op, where TVTV is the Heyting algebra of truth values.

Mere and pure comparisons

In dependent type theory, there are two different notions of a cotransitive or weakly linear relation

  • There is the traditional interpretation of a cotransitive or weakly linear relation which uses the disjunction, and is called a merely cotransitive relation or merely weakly linear relation or a mere comparison
x,y,z:Axz(xyyz)\prod_{x, y, z: A} x \sim z \to (x \sim y \vee y \sim z)
  • There is the traditional interpretation of a cotransitive or weakly linear relation which uses the sum type to represent inclusive or, and is called a purely cotransitive relation or purely weakly linear relation or a pure comparison or a constructively cotransitive relation or constructively weakly linear relaiton or a constructive comparison
x,y,z:Axz(xy+yz)\prod_{x, y, z: A} x \sim z \to (x \sim y + y \sim z)

This distinction could also be made in set theory: Given a proposition PP, PP can be made into a subsingleton set by considering the subset {|P}{p{}|(p=)P}\{\top \vert P\} \coloneqq \{p \in \{\top\} \vert (p = \top) \wedge P\} of the singleton {}\{\top\}. Let [A][A] denote the support of the set AA, and let ABA \uplus B denote the disjoint union of sets AA and BB. Then

  • a merely cotransitive relation or merely weakly linear relation on a set AA is a relation \sim which for all xx, yy, and zz one can construct an element
cotransitive(x,y,z)[{|xy}{|yz}] {|xz}\mathrm{cotransitive}(x, y, z) \in \left[\{\top \vert x \sim y\} \uplus \{\top \vert y \sim z\}\right]^{\{\top \vert x \sim z\}}
  • a purely cotransitive relation or purely weakly linear relation or constructively cotransitive relation or constructively weakly linear relation on a set AA is a relation \sim which for all xx, yy, and zz one can construct an element
cotransitive(x,y,z)({|xy}{|yz}) {|xz}\mathrm{cotransitive}(x, y, z) \in \left(\{\top \vert x \sim y\} \uplus \{\top \vert y \sim z\}\right)^{\{\top \vert x \sim z\}}

References

Last revised on September 25, 2024 at 22:24:36. See the history of this page for a list of all contributions to it.