Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
Roughly, $Rel$ is the category whose objects are sets and whose morphisms are (binary) relations between sets. It becomes a 2-category (in fact, a 2-poset) by taking 2-morphisms to be inclusions of relations.
$Rel$ is a 2-poset (a category enriched in the category of posets), whose objects or $0$-cells are sets, whose morphisms or $1$-cells $X \to Y$ are relations $R \subseteq X \times Y$, and whose 2-morphisms or $2$-cells $R \to S$ are inclusions of relations. The composite $S \circ R$ of morphisms $R: X \to Y$ and $S: Y \to Z$ is defined by the usual relational composite
and the identity $1_X: X \to X$ is the equality relation, in other words the usual diagonal embedding
Another important operation on relations is taking the opposite: any relation $R: X \to Y$ induces a relation
and this operation obeys a number of obvious identities, such as $(S \circ R)^{op} = R^{op} \circ S^{op}$ and $1_X^{op} = 1_X$.
It is useful to be aware of the connections between the bicategory of relations and the bicategory of spans. Recall that a span from $X$ to $Y$ is a diagram of the form
and there is an obvious category whose objects are spans from $X$ to $Y$ and whose morphisms are morphisms between such diagrams. The terminal span from $X$ to $Y$ is
and a relation from $X$ to $Y$ is just a subobject of the terminal span, in other words an isomorphism class of monos into the terminal span.
To each span $S$ from $X$ to $Y$, there is a corresponding relation from $X$ to $Y$, defined by taking the image of the unique morphism of spans $S \to X \times Y$ between $X$ and $Y$. It may be checked that this yields a lax morphism of bicategories
More generally, given any regular category $C$, one can form a 2-category of relations $Rel(C)$ in similar fashion. The objects of $Rel(C)$ are objects of $C$, the morphisms $r: c \to d$ in $Rel(C)$ are defined to be subobjects of the terminal span from $c$ to $d$, and 2-cells $r \to s$ are subobject inclusions. To form the composite of $r \subseteq c \times d$ and $s \subseteq d \times e$, one takes the image of the unique span morphism
in the category of spans from $c$ to $e$, thus giving a mono into the terminal span from $c$ to $e$. The subobject class of this mono defines the relation
and the axioms of a regular category ensure that $Rel(C)$ is a 2-category with desirable properties. Similar to what was said above, there is again a lax morphism of bicategories
There is also a functor
that takes a morphism $f: c \to d$ to the functional relation defined by $f$, i.e., the relation defined by the subobject class of the mono
Such functional relations may also be characterized as precisely those 1-cells in $Rel(C)$ which are left adjoints; the right adjoint of $\langle 1, f \rangle$ is the opposite relation $\langle f, 1\rangle$. The unit amounts to a condition
which says that the functional relation is total, and the counit amounts to a condition
which says the functional relation is well-defined.
A category of correspondences is a generalization of a category of relations. The composition of relations is that of correspondences followed by (-1)-truncation.
For generalizations of $Rel$ see