The category of relations with apartness composition is the category $\mathsf{Rel}^{\mathord {\mathbin {\square }}}$ where
-
•
Objects. The objects of $\mathsf{Rel}^{\mathord {\mathbin {\square }}}$ are sets.
-
•
Morphisms. For each $A,B\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, we have
\[ \mathsf{Rel}^{\mathord {\mathbin {\square }}}(A,B) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathrm{Rel}(A,B). \] -
•
Identities. For each $A\in \operatorname {\mathrm{Obj}}(\mathsf{Rel}^{\mathord {\mathbin {\square }}})$, the unit map
\[ \mathbb {1}^{\mathsf{Rel}^{\mathord {\mathbin {\square }}}}_{A} \colon \mathrm{pt}\to \mathrm{Rel}(A,A) \]of $\mathsf{Rel}^{\mathord {\mathbin {\square }}}$ at $A$ is defined by
\[ \operatorname {\mathrm{id}}^{\mathsf{Rel}^{\mathord {\mathbin {\square }}}}_{A} \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\nabla _{A}(-_{1},-_{2}), \]where $\nabla _{A}(-_{1},-_{2})$ is the antidiagonal relation of $A$ of Example 8.2.1.1.4.
-
•
Composition. For each $A,B,C\in \operatorname {\mathrm{Obj}}(\mathsf{Rel}^{\mathord {\mathbin {\square }}})$, the composition map
\[ \circ ^{\mathsf{Rel}^{\mathord {\mathbin {\square }}}}_{A,B,C}\colon \mathrm{Rel}(B,C)\times \mathrm{Rel}(A,B)\to \mathrm{Rel}(A,C) \]of $\mathsf{Rel}^{\mathord {\mathbin {\square }}}$ at $(A,B,C)$ is defined by
\[ S\mathbin {{\circ }^{\mathsf{Rel}^{\mathord {\mathbin {\square }}}}_{A,B,C}}R \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}S\mathbin {\square }R \]for each $(S,R)\in \mathrm{Rel}(B,C)\times \mathrm{Rel}(A,B)$, where $S\mathbin {\diamond }R$ is the composition of $S$ and $R$ of Definition 8.1.4.1.1.
