Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
A binary relation on a set is tight if for all elements and , implies that .
Every tight relation is a connected relation. Every connected symmetric relation is a tight relation.
Sometimes in constructive mathematics, what matters for a relation is not that the negation implies equality, but the negation implies the double negation of equality. Such a relation is called weakly tight.
A binary relation on a set is weakly tight if for all elements and , implies that . By intuitionistic contraposition, this implies that for all elements and , implies that .
Important examples of weakly tight relations include denial inequality.
An irreflexive relation with terms is tight if the canonical function
inductively defined by
is an equivalence of types
Created on December 8, 2022 at 17:08:57. See the history of this page for a list of all contributions to it.