The Clowder Project

Let $f\colon A\to B$ be a function.

1. Functoriality. The assignment $A\mapsto A$, $f\mapsto f^{-1}$ defines a functor
   \[ \webleft (-\webright )^{-1}\colon \mathsf{Sets}\to \mathrm{Rel} \]

   where

   • Action on Objects. For each $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, we have
     \[ \webleft[\webleft (-\webright )^{-1}\webright]\webleft (A\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}A. \]

   • Action on Morphisms. For each $A,B\in \text{Obj}\webleft (\mathsf{Sets}\webright )$, the action on $\textup{Hom}$-sets
     \[ \webleft (-\webright )^{-1}_{A,B}\colon \mathsf{Sets}\webleft (A,B\webright ) \to \mathrm{Rel}\webleft (A,B\webright ) \]

     of $\webleft (-\webright )^{-1}$ at $\webleft (A,B\webright )$ is defined by

     \[ \webleft (-\webright )^{-1}_{A,B}\webleft (f\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft[\webleft (-\webright )^{-1}\webright]\webleft (f\webright ), \]

     where $f^{-1}$ is the inverse of $f$ as in Definition 6.3.2.1.1.

   In particular:
   • Preservation of Identities. We have
     \[ \text{id}^{-1}_{A}=\chi _{A} \]

     for each $A\in \text{Obj}\webleft (\mathsf{Sets}\webright )$.

   • Preservation of Composition. We have
     \[ \webleft (g\circ f\webright )^{-1}=g^{-1}\mathbin {\diamond }f^{-1} \]

     for pair of functions $f\colon A\to B$ and $g\colon B\to C$.

2. Adjointness Inside $\textbf{Rel}$. We have an adjunction
   
   in $\textbf{Rel}$.
3. Interaction With Inverses of Relations. We have
   \begin{align*} \webleft (f^{-1}\webright )^{\dagger } & = \text{Gr}\webleft (f\webright ),\\ \text{Gr}\webleft (f\webright )^{\dagger } & = f^{-1}. \end{align*}