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.

Extending Remark 6.1.2.1.1, the equivalent definitions of relations in are also related to the corresponding ones for profunctors (), which state that a profunctor $\mathfrak {p}\colon \mathcal{C}\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}\mathcal{D}$ is equivalently:

1. A functor $\mathfrak {p}\colon \mathcal{D}^{\mathsf{op}}\times \mathcal{C}\to \mathsf{Sets}$.
2. A functor $\mathfrak {p}\colon \mathcal{C}\to \mathsf{PSh}\webleft (\mathcal{D}\webright )$.
3. A functor $\mathfrak {p}\colon \mathcal{D}^{\mathsf{op}}\to \mathsf{Fun}\webleft (\mathcal{C},\mathsf{Sets}\webright )$.
4. A colimit-preserving functor $\mathfrak {p}\colon \mathsf{PSh}\webleft (\mathcal{C}\webright )\to \mathsf{PSh}\webleft (\mathcal{D}\webright )$.

Indeed:

• The equivalence between Item 1 and Item 2 (and also that between Item 1 and Item 3, which is proved analogously) is an instance of currying, both for profunctors as well as for relations, using the isomorphisms
  \begin{align*} \mathsf{Sets}\webleft (A\times B,\{ \mathsf{true},\mathsf{false}\} \webright ) & \cong \mathsf{Sets}\webleft (A,\mathsf{Sets}\webleft (B,\{ \mathsf{true},\mathsf{false}\} \webright )\webright )\\ & \cong \mathsf{Sets}\webleft (A,\mathcal{P}\webleft (B\webright )\webright ),\\ \mathsf{Fun}\webleft (\mathcal{D}^{\mathsf{op}}\times \mathcal{D},\mathsf{Sets}\webright ) & \cong \mathsf{Fun}\webleft (\mathcal{C},\mathsf{Fun}\webleft (\mathcal{D}^{\mathsf{op}},\mathsf{Sets}\webright )\webright )\\ & \cong \mathsf{Fun}\webleft (\mathcal{C},\mathsf{PSh}\webleft (\mathcal{D}\webright )\webright ). \end{align*}

• The equivalence between Item 1 and Item 3 follows from the universal properties of:
  • The powerset $\mathcal{P}\webleft (X\webright )$ of a set $X$ as the free cocompletion of $X$ via the characteristic embedding
    \[ \chi _{\webleft (-\webright )} \colon X \hookrightarrow \mathcal{P}\webleft (X\webright ) \]

    of $X$ into $\mathcal{P}\webleft (X\webright )$, as stated and proved in Chapter 2: Constructions With Sets, of .

  • The category $\mathsf{PSh}\webleft (\mathcal{C}\webright )$ of presheaves on a category $\mathcal{C}$ as the free cocompletion of $\mathcal{C}$ via the Yoneda embedding
    \[ {\text{よ}}\colon \mathcal{C} \hookrightarrow \mathsf{PSh}\webleft (\mathcal{C}\webright ) \]

    of $\mathcal{C}$ into $\mathsf{PSh}\webleft (\mathcal{C}\webright )$, as stated and proved in of .