The Clowder Project

The 2-category of relations with apartness composition is the locally posetal 2-category $\boldsymbol {\mathsf{Rel}}$ where

• •

  Objects. The objects of $\boldsymbol {\mathsf{Rel}}$ are sets.

• •

  $\mathbf{Hom}$-Objects. For each $A,B\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, we have

  \begin{align*} \operatorname {\mathrm{Hom}}_{\boldsymbol {\mathsf{Rel}}}(A,B) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathbf{Rel}(A,B)\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}(\mathrm{Rel}(A,B),\subset ).\end{align*}
• •

  Identities. For each $A\in \operatorname {\mathrm{Obj}}(\boldsymbol {\mathsf{Rel}})$, the unit map

  \[ \mathbb {1}^{\boldsymbol {\mathsf{Rel}}}_{A} \colon \mathrm{pt}\to \mathbf{Rel}(A,A) \]

  of $\boldsymbol {\mathsf{Rel}}$ at $A$ is defined by

  \[ \operatorname {\mathrm{id}}^{\boldsymbol {\mathsf{Rel}}}_{A} \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\chi _{A}(-_{1},-_{2}), \]

  where $\chi _{A}(-_{1},-_{2})$ is the characteristic relation of $A$ of Example 8.2.1.1.3.

• •

  Composition. For each $A,B,C\in \operatorname {\mathrm{Obj}}(\boldsymbol {\mathsf{Rel}})$, the composition map¹

  \[ \circ ^{\boldsymbol {\mathsf{Rel}}}_{A,B,C}\colon \mathbf{Rel}(B,C)\times \mathbf{Rel}(A,B)\to \mathbf{Rel}(A,C) \]

  of $\boldsymbol {\mathsf{Rel}}$ at $(A,B,C)$ is defined by

  \[ S\mathbin {{\circ }^{\boldsymbol {\mathsf{Rel}}}_{A,B,C}}R \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}S\mathbin {\diamond }R \]

  for each $(S,R)\in \boldsymbol {\mathsf{Rel}}(B,C)\times \boldsymbol {\mathsf{Rel}}(A,B)$, where $S\mathbin {\diamond }R$ is the composition of $S$ and $R$ of Definition 8.1.3.1.1.