The Clowder Project

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

1. 1.

   Functoriality. The assignment $A\mapsto A$, $f\mapsto f^{-1}$ defines a functor

   \[ (-)^{-1}\colon \mathsf{Sets}\to \mathrm{Rel} \]

   where

   • •

     Action on Objects. For each $A\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, we have

     \[ \left[(-)^{-1}\right](A)\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}A. \]
   • •

     Action on Morphisms. For each $A,B\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$, the action on $\operatorname {\mathrm{Hom}}$-sets

     \[ (-)^{-1}_{A,B}\colon \mathsf{Sets}(A,B) \to \mathrm{Rel}(A,B) \]

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

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

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

   In particular, the following statements are true:

   • •

     Preservation of Identities. We have

     \[ \operatorname {\mathrm{id}}^{-1}_{A}=\chi _{A} \]

     for each $A\in \operatorname {\mathrm{Obj}}(\mathsf{Sets})$.

   • •

     Preservation of Composition. We have

     \[ (g\circ f)^{-1}=g^{-1}\mathbin {\diamond }f^{-1} \]

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

2. 2.

   Adjointness Inside $\boldsymbol {\mathsf{Rel}}$. We have an adjunction

   
   in $\boldsymbol {\mathsf{Rel}}$.

3. 3.

   Interaction With Converses of Relations. We have

   \begin{align*} (f^{-1})^{\dagger } & = \operatorname {\mathrm{Gr}}(f),\\ \operatorname {\mathrm{Gr}}(f)^{\dagger } & = f^{-1}. \end{align*}