nLab comparison

 Definition

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

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

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

Alternatively, this is the same condition as

$$\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^\op$, where $TV$ 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

$$\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

$$\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 $P$, $P$ can be made into a subsingleton set by considering the subset $\{\top \vert P\} \coloneqq \{p \in \{\top\} \vert (p = \top) \wedge P\}$ of the singleton $\{\top\}$. Let $[A]$ denote the support of the set $A$, and let $A \uplus B$ denote the disjoint union of sets $A$ and $B$. Then

• a merely cotransitive relation or merely weakly linear relation on a set $A$ is a relation $\sim$ which for all $x$, $y$, and $z$ one can construct an element

$$\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 $A$ is a relation $\sim$ which for all $x$, $y$, and $z$ one can construct an element

$$\mathrm{cotransitive}(x, y, z) \in \left(\{\top \vert x \sim y\} \uplus \{\top \vert y \sim z\}\right)^{\{\top \vert x \sim z\}}$$

 Related concepts

• pseudo-order

• total relation

References

• 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$]$