nLab
(infinity, 1)Prof

Contents

Definition

(,1)Prof\mathbf{(\infty, 1)Prof} is the (∞,2)-category of (∞,1)-categories, (∞,1)-profunctors, and natural transformations.

Recall that a (∞,1)-profunctor from AA to BB is a (∞,1)-functor B op×AGrpdB^{op}\times A\to \infty Grpd. Composition of (∞,1)-profunctors in (,1)Prof(\infty, 1)Prof is by the “tensor product of (∞,1)-functors” homotopy coend construction: if H:AUnknown characterUnknown characterUnknown characterBH\colon A ⇸ B and K:BUnknown characterUnknown characterUnknown characterCK\colon B ⇸ C, their composite is given as a functor C op×AGrpdC^{op}\times A \to \infty Grpd 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 an (∞,1)-category AA is its hom-functor Hom A(,)Hom_A(-,-).

Properties

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

(,1)Prof(\infty, 1)Prof can act as a classifying object for kinds of (∞,1)-functors; see higher exponentiable functor.

(,1)Prof(\infty,1)Prof is equivalent to the full subcategory of Pr(∞,1)Cat whose objects are presheaf categories.

References

Revised on August 25, 2017 03:14:17 by David Corfield (209.93.199.101)