Profunctor (programming)

In category theory, a branch of mathematics, profunctors are a generalization of relations and also of bimodules.

Definition

A profunctor (also named distributor by the French school and module by the Sydney school) $\,\phi$ from a category $C$ to a category $D$, written
: $\phi : C\nrightarrow D$,
is defined to be a functor
: $\phi : D^\times C\to\mathbf$
where $D^\mathrm$ denotes the opposite category of $D$ and $\mathbf$ denotes the category of sets. Given morphisms $f : d\to d', g : c\to c'$ respectively in $D, C$ and an element $x\in\phi(d',c)$, we write $xf\in \phi(d,c), gx\in\phi(d',c')$ to denote the actions.

Using the cartesian closure of $\mathbf$, the category of small categories, the profunctor $\phi$ can be seen as a functor
: $\hat : C\to\hat$
where $\hat$ denotes the category $\mathrm^$ of presheaves over $D$.

A correspondence from $C$ to $D$ is a profunctor $D\nrightarrow C$.

Profunctors as categories

An equivalent definition of a profunctor $\phi : C\nrightarrow D$ is a category whose objects are the disjoint union of the objects of $C$ and the objects of $D$, and whose morphisms are the morphisms of $C$ and the morphisms of $D$, plus zero or more additional morphisms from objects of $D$ to objects of $C$. The sets in the formal definition above are the hom-sets between objects of $D$ and objects of $C$. (These are also known as het-sets, since the corresponding morphisms can be called ''heteromorphisms''.) The previous definition can be recovered by the restriction of the hom-functor $\phi^\text\times \phi \to \mathbf$ to $D^\text\times C$.

This also makes it clear that a profunctor can be thought of as a relation between the objects of $C$ and the objects of $D$, where each member of the relation is associated with a set of morphisms. A functor is a special case of a profunctor in the same way that a function is a special case of a relation.

Composition of profunctors

The composite $\psi\phi$ of two profunctors
: $\phi : C\nrightarrow D$ and $\psi : D\nrightarrow E$
is given by
: $\psi\phi=\mathrm_(\hat)\circ\hat\phi$
where $\mathrm_(\hat)$ is the left Kan extension of the functor $\hat$ along the Yoneda functor $Y_D : D\to\hat D$ of $D$ (which to every object $d$ of $D$ associates the functor $D(-,d) : D^\to\mathrm$).

It can be shown that
: $(\psi\phi)(e,c)=\left(\coprod_\psi(e,d)\times\phi(d,c)\right)\Bigg/\sim$
where $\sim$ is the least equivalence relation such that $(y',x')\sim(y,x)$ whenever there exists a morphism $v$ in $D$ such that
: $y'=vy \in\psi(e,d')$ and $x'v=x \in\phi(d,c)$.
Equivalently, profunctor composition can be written using a coend
: $(\psi\phi)(e,c)=\int^\psi(e,d)\times\phi(d,c)$

Bicategory of profunctors

Composition of profunctors is associative only up to isomorphism (because the product is not strictly associative in Set). The best one can hope is therefore to build a bicategory Prof whose
* 0-cells are small categories,
* 1-cells between two small categories are the profunctors between those categories,
* 2-cells between two profunctors are the natural transformations between those profunctors.

Properties

Lifting functors to profunctors

A functor $F : C\to D$ can be seen as a profunctor $\phi_F : C\nrightarrow D$ by postcomposing with the Yoneda functor:
: $\phi_F=Y_D\circ F$.

It can be shown that such a profunctor $\phi_F$ has a right adjoint. Moreover, this is a characterization: a profunctor $\phi : C\nrightarrow D$ has a right adjoint if and only if $\hat\phi : C\to\hat D$ factors through the Cauchy completion of $D$, i.e. there exists a functor $F : C\to D$ such that $\hat\phi=Y_D\circ F$.

See also

*Anafunctor

References

*
*
*
*
*
{{refend

Functors