The Clowder Project

The notion of a relation is a decategorification of that of a profunctor:

1. A profunctor from a category $\mathcal{C}$ to a category $\mathcal{D}$ is a functor
   \[ \mathfrak {p}\colon \mathcal{D}^{\mathsf{op}}\times \mathcal{C}\to \mathsf{Sets}. \]
2. A relation on sets $A$ and $B$ is a function
   \[ R\colon A\times B\to \{ \mathsf{true},\mathsf{false}\} . \]

Here we notice that:

• The opposite $X^{\mathsf{op}}$ of a set $X$ is itself, as $\webleft (-\webright )^{\mathsf{op}}\colon \mathsf{Cats}\to \mathsf{Cats}$ restricts to the identity endofunctor on $\mathsf{Sets}$.
• The values that profunctors and relations take are analogous:
  • A category is enriched over the category
    \[ \mathsf{Sets}\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathsf{Cats}_{0} \]

    of sets, with profunctors taking values on it.

  • A set is enriched over the set
    \[ \{ \mathsf{true},\mathsf{false}\} \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathsf{Cats}_{-1} \]

    of classical truth values, with relations taking values on it.