The Clowder Project

The double category of relations is the locally posetal double category $\smash {\mathsf{Rel}^{\mathsf{dbl}}}$ where

• •

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

• •

  Vertical Morphisms. The vertical morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$ are maps of sets $f\colon A\to B$.

• •

  Horizontal Morphisms. The horizontal morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$ are relations $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}X$.

• •

  $2$-Morphisms. A $2$-cell

  
  of $\mathsf{Rel}^{\mathsf{dbl}}$ is either non-existent or an inclusion of relations of the form
  

• •

  Horizontal Identities. The horizontal unit functor of $\mathsf{Rel}^{\mathsf{dbl}}$ is the functor of Definition 8.3.5.2.1.

• •

  Vertical Identities. For each $A\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Rel}^{\mathsf{dbl}}\webright )$, we have

  \[ \operatorname {\mathrm{id}}^{\mathsf{Rel}^{\mathsf{dbl}}}_{A} \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {\mathrm{id}}_{A}. \]
• •

  Identity $2$-Morphisms. For each horizontal morphism $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ of $\mathsf{Rel}^{\mathsf{dbl}}$, the identity $2$-morphism

  
  of $R$ is the identity inclusion
  

• •

  Horizontal Composition. The horizontal composition functor of $\mathsf{Rel}^{\mathsf{dbl}}$ is the functor of Definition 8.3.5.3.1.

• •

  Vertical Composition of $1$-Morphisms. For each composable pair $A\smash {\overset {F}{\to }}B\smash {\overset {G}{\to }}C$ of vertical morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$, i.e. maps of sets, we have

  \[ g\mathbin {{\circ }^{\mathsf{Rel}^{\mathsf{dbl}}}}f \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}g\circ f. \]
• •

  Vertical Composition of $2$-Morphisms. The vertical composition of $2$-morphisms in $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as in Definition 8.3.5.4.1.

• •

  Associators. The associators of $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as in Definition 8.3.5.5.1.

• •

  Left Unitors. The left unitors of $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as in Definition 8.3.5.6.1.

• •

  Right Unitors. The right unitors of $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as in Definition 8.3.5.7.1.

The horizontal unit functor of $\mathsf{Rel}^{\mathsf{dbl}}$ is the functor

of $\mathsf{Rel}^{\mathsf{dbl}}$ is the functor where

• •

  Action on Objects. For each $A\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Rel}^{\mathsf{dbl}}_{0}\webright )$, we have

  \[ \mathbb {1}_{A} \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\chi _{A}\webleft (-_{1},-_{2}\webright ). \]
• •

  Action on Morphisms. For each vertical morphism $f\colon A\to B$ of $\mathsf{Rel}^{\mathsf{dbl}}$, i.e. each map of sets $f$ from $A$ to $B$, the identity $2$-morphism

  
  of $f$ is the inclusion
  
  of Chapter 4: Constructions With Sets, Item 1 of Proposition 4.5.3.1.3.

The horizontal composition functor of $\mathsf{Rel}^{\mathsf{dbl}}$ is the functor

of $\mathsf{Rel}^{\mathsf{dbl}}$ is the functor where

• •

  Action on Objects. For each composable pair $\smash {A\mathbin {\overset {R}{\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}}}B\mathbin {\overset {S}{\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}}}C}$ of horizontal morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$, we have

  \[ S\mathbin {\odot }R\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}S\mathbin {\diamond }R, \]

  where $S\mathbin {\diamond }R$ is the composition of $R$ and $S$ of Chapter 9: Constructions With Relations, .

• •

  Action on Morphisms. For each horizontally composable pair

  
  of $2$-morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$, i.e. for each pair
  
  of inclusions of relations, the horizontal composition
  
  of $\alpha $ and $\beta $ is the inclusion of relations¹
  

The vertical composition in $\mathsf{Rel}^{\mathsf{dbl}}$ is defined as follows: for each vertically composable pair

For each composable triple

of horizontal morphisms of $\mathsf{Rel}^{\mathsf{dbl}}$, the component

For each horizontal morphism $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ of $\mathsf{Rel}^{\mathsf{dbl}}$, the component