nLab Prof




Prof\mathbf{Prof} is the 2-category of categories, profunctors, and natural transformations.

Recall that a profunctor from AA to BB is a functor B op×ASetB^{op}\times A\to Set. Composition of profunctors in ProfProf is by the “tensor product of functors” coend construction: if H:ABH\colon A\to B and K:BCK\colon B\to C, their composite is given as a functor C op×ASetC^{op}\times A \to Set by

(c,a) bBH(b,a)×K(c,b).(c,a)\mapsto \int^{b\in B} H(b,a)\times K(c,b).

The identity on a category AA is its hom-functor Hom A(,)Hom_A(-,-).

Prof\mathbf{Prof} can also be obtained as the Kleisli 2-category of PSh.


If profunctors are categorified binary relations, then ProfProf is a categorification of Rel.

Note that as defined here, ProfProf is a weak 22-category or bicategory. A naturally defined equivalent strict 2-category has the same objects, but the morphisms ABA\to B are cocontinuous functors PAPBP A \to P B, where PAP A is the presheaf category of AA. This is equivalent because a profunctor ABA\to B can equivalently be regarded as a functor APBA\to P B, and PAP A is the free cocompletion of AA. This equivalence is an instance of Lack's coherence theorem.

Note that every functor f:ABf\colon A\to B gives two representable profunctors B(f,)B(f-,-) and B(,f)B(-,f-). This defines two 2-functors CatProfCat \to Prof that are the identity on objects. The relationship between Cat and ProfProf encoded in this way makes them into an equipment.

ProfProf is a sort of classifying object for arbitrary functors; see displayed category.

There are also enriched and internal versions of ProfProf. These accordingly refine categories of enriched categories.

ProfProf is a locally cocomplete bicategory.


category: category

Last revised on February 16, 2024 at 13:44:18. See the history of this page for a list of all contributions to it.