The Clowder Project

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 \text{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 2: Constructions With Sets, of .