Category of relations ($\mathbf{Rel}$)

For a regular category $\mathcal{C}$, the category $\mathbf{Rel}(\mathcal{C})$ has the objects of $\mathcal{C}$ and subobjects of $A\times B$ as relations $A⇝B$. Composition takes the image of the pullback expressing existential quantification over the middle object.

For $\mathcal{C}=\mathbf{Set}$ this is the category of relations (sets); the general construction also applies to other regular categories.

The category of relations on sets has sets as objects and binary relations as morphisms. Relational composition declares $aRc$ when some intermediate $b$ satisfies both component relations; the identity is the diagonal relation.

In a regular category, a relation $R\hookrightarrow A\times B$ is total if its projection to $A$ is a regular epimorphism, and single-valued if two pairs with the same first component have the same second component. The latter makes that projection a monomorphism. A regular epimorphism that is monic is invertible, so $f={\pi }_B{\pi }_A^{-1}$ has graph exactly $R$. No axiom of choice or set-based element selection is used.

The graph of $f:A\to B$ is the relation represented by $(1_A,f):A\hookrightarrow A\times B$. Its converse is right adjoint to it in the pointwise order on relations.