The Clowder Project

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 .