Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
A (binary) relation $\sim$ on a set $A$ is irreflexive if no element of $A$ is related to itself:
In the language of the $2$-poset Rel of sets and relations, a relation $R: A \to A$ is irreflexive if it is disjoint? from the identity relation on $A$:
Of course, this containment is in fact an equality.
In constructive mathematics, if $A$ is equipped with a tight apartness $\#$, we say that $\sim$ is strongly irrelexive if only distinct elements of $A$ are related:
Since $\#$ is irrelexive itself, any strongly irrelexive relation must be irrelexive. The converse holds using excluded middle, through which every set has a unique tight apartness.