Prof (changes) in nLab

Showing changes from revision #10 to #11: Added | Removed | Changed

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×A→SetB^{op}\times A\to Set. Composition of profunctors in ProfProf is by the “tensor product of functors” coend construction: if H:A→BH\colon A\to B and K:B→CK\colon B\to C, their composite is given as a functor C op×A→SetC^{op}\times A \to Set by

(c,a)↦∫ b∈BH(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.

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 A→BA\to B are cocontinuous functors PA→PBP A \to P B, where PAP A is the presheaf category of AA. This is equivalent because a profunctor A→BA\to B can equivalently be regarded as a functor A→PBA\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:A→Bf\colon A\to B gives two representable profunctors B(f−,−)B(f-,-) and B(−,f−)B(-,f-). This defines two 2-functors Cat→ProfCat \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.

• Pos

• Set

  • Rel, Span, Prof

• Grpd, ∞Grpd

• Cat,

  • Operad

  • VCat

• 2Cat

• (∞,1)Cat

  • (∞,1)Operad

• (∞,n)Cat

References

• Maren Justesen, Bikategorien af Profunktorer, Aarhus 1968 (pdf)