Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
A (binary) relation on a set is connected if any two elements that are related in neither order are equal:
This is a basic property of linear orders; an apartness relation is usually called tight if it is connected.
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, 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 is already equipped with a tight apartness . In that case, we say that 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).