Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
basic constructions:
strong axioms
further
An irreflexive symmetric relation is a binary relation that is irreflexive and symmetric.
Every apartness relation is an irreflexive symmetric relation which is also a comparison.
The negation of a reflexive symmetric relation is an irreflexive symmetric relation.
Every denial inequality is a weakly tight irreflexive symmetric relation.
In constructive mathematics, not ever tight irreflexive symmetric relation is a denial inequality, and not every denial inequality is tight. Instead, every denial inequality is only weakly tight. Indeed, since excluded middle cannot be proven, we could distinguish between the following irreflexive symmetric relations in constructive mathematics:
denial inequality, an irreflexive symmetric relation $\neq$ which additionally satisfies $\neg(a = b)$ implies $(a \neq b)$
tight irreflexive symmetric relation, an irreflexive symmetric relation $\neq$ which additionally satisfies $\neg(a \neq b)$ implies $(a = b)$
weakly tight irreflexive symmetric relation, an irreflexive symmetric relation $\neq$ which additionally satisfies $\neg(a \neq b)$ implies $\neg \neg (a = b)$
stable irreflexive symmetric relation, an irreflexive symmetric relation $\neq$ which additionally satisfies $\neg \neg (a \neq b)$ implies $(a \neq b)$
decidable irreflexive symmetric relation, an irreflexive symmetric relation $\neq$ which additionally satisfies $(a \neq b)$ or $\neg (a \neq b)$
apartness relation, an irreflexive symmetric relation $\neq$ which additionally satisfies $a \neq b$ implies that $a \neq c$ or $c \neq b$
or any combination of the above, such as tight apartness relation.
The notion of “inequality relation” in constructive mathematics usually refers to either the denial inequality or a tight apartness relation. On the other hand, some authors have used “inequality relation” to refere to general irreflexive symmetric relations.
Last revised on December 8, 2022 at 20:36:15. See the history of this page for a list of all contributions to it.