Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
A binary relation $R$ on a set $A$ is tight if for all elements $a \in A$ and $b \in A$, $\neg R(a, b)$ implies that $a = b$.
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 $R$ on a set $A$ is weakly tight if for all elements $a \in A$ and $b \in A$, $\neg R(a, b)$ implies that $\neg \neg (a = b)$. By intuitionistic contraposition, this implies that for all elements $a \in A$ and $b \in A$, $\neg (a = b)$ implies that $\neg \neg R(a, b)$.
Important examples of weakly tight relations include denial inequality.
An irreflexive relation $\sim$ with terms $a:A \vdash \mathrm{irr}(a):(a \sim a) \to \emptyset$ 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.