Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
A (binary) relation $\sim$ on a set $A$ is connected (or sometimes linear) if any two elements that are related in neither order are equal:
This is a basic property of linear orders.
Every tight relation is a connected relation. Every connected symmetric relation is a tight relation.
Using excluded middle, it is equivalent to say that every two elements are related in some order or equal:
However, this version is too strong for the intended applications to constructive mathematics. (In particular, $\lt$ on the located Dedekind real numbers satisfies the first definition but not this one.)
On the other hand, there is a stronger notion that may be used in constructive mathematics, if $A$ is already equipped with a tight apartness $\#$. In that case, we say that $\sim$ is strongly connected if any two distinct elements are related in one order or the other:
Since $\#$ is connected itself, every strongly connected relation is connected; the converse holds with excluded middle (through which every set has a unique tight apartness).
We can do a similar thing if $A$ is equipped with any inequality $\#$, except that in the general case, this is not necessarily stronger than being connected, and so we should call it $\#$-connected.
In dependent type theory, an irreflexive relation $\sim$ with terms $a:A \vdash \mathrm{irr}(a):(a \sim a) \to \emptyset$ is connected if the canonical function
inductively defined by
is an equivalence of types
Last revised on December 8, 2022 at 17:14:43. See the history of this page for a list of all contributions to it.