nLab
Prof

Contents

Definition

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(-,-).

Properties

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.

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

category: category

Revised on October 30, 2012 20:00:54 by Urs Schreiber (131.174.189.66)