Yoneda lemma for bicategories



Yoneda lemma

2-category theory



The Yoneda lemma for bicategories is a version of the Yoneda lemma that applies to bicategories, the most common algebraic sort of weak 2-category. It says that for any bicategory CC, any object xCx\in C, and any pseudofunctor F:C opCatF\colon C^{op}\to Cat, there is an equivalence of categories

[C op,Cat](C(,x),F)F(x) [C^{op},Cat](C(-,x), F) \simeq F(x)

which is pseudonatural in xx and FF, and which is given by evaluation at 1 x1_x, i.e. α:C(,x)F\alpha\colon C(-,x)\to F maps to α x(1 x)\alpha_x(1_x).

For bicategories AA and BB, [A,B][A,B] denotes the bicategory of pseudofunctors, pseudonatural transformations, and modifications from AA to BB. Note that it is a strict 2-category as soon as BB is.


In particular, the Yoneda lemma for bicategories implies that there is a Yoneda embedding for bicategories C[C op,Cat]C\to [C^{op},Cat] which is 2-fully-faithful?, i.e. an equivalence on hom-categories. Therefore, CC is equivalent to a sub-bicategory of [C op,Cat][C^{op},Cat]. Since Cat is a strict 2-category, it follows that CC is equivalent to a strict 2-category, which is one form of the coherence theorem for bicategories. (Conversely, another form of the coherence theorem can be used to prove the Yoneda lemma; see below.)


A detailed proof of the bicategorical Yoneda lemma is given in (Johnson & Yau 20, Chap. 8).

Explicit proof

An explicit proof, involving many diagrams, has been written up by Igor Baković and can be found here.

High-technology proof

We will take it for granted that [C op,Cat][C^{op},Cat] is a well-defined bicategory; this is a basic fact having nothing to do with the Yoneda lemma. We also take it as given that “evaluation at 1 x1_x” functor

[C op,Cat](C(,x),F)F(x) [C^{op},Cat](C(-,x), F) \to F(x)

is well-defined and pseudonatural in FF and xx; our goal is to prove that it is an equivalence. (Granted, these basic facts require a fair amount of verification as well.)

We will use part of the coherence theorem for pseudoalgebras?, which says that for a suitably well-behaved strict 2-monad TT, the inclusion TT-Alg strictPsAlg_{strict} \hookrightarrow Ps-TT-AlgAlg of the 2-category of strict TT-algebras and strict TT-morphisms into the 2-category of pseudo TT-algebras and pseudo TT-morphisms has a left adjoint, usually written as ()(-)'. Moreover, for any pseudo TT-algebra AA, the unit AAA\to A' is an equivalence in PsPs-TT-AlgAlg.

First, there is a 2-monad TT such that strict TT-algebras are strict 2-categories, strict TT-morphisms are strict 2-functors, pseudo TT-algebras are unbiased bicategories, and pseudo TT-morphisms are pseudofunctors. By Mac Lane’s coherence theorem for bicategories, any ordinary bicategory can equally well be considered as an unbiased one. Thus, since CatCat is a strict 2-category, for any bicategory CC there is a strict 2-category CC' such that pseudofunctors CCatC\to Cat are in bijection with strict 2-functors CCatC'\to Cat.

Now note that a pseudonatural transformation between two pseudofunctors (resp. strict 2-functors) CDC\to D is the same as a single pseudofunctor (resp. strict 2-functor) CCyl(D)C\to Cyl(D), where Cyl(D)Cyl(D) is the bicategory whose objects are the 1-cells of DD, whose 1-cells are squares in DD commuting up to isomorphism, and whose 2-cells are “cylinders” in DD. Likewise, a modification between two such transformations is the same as a single functor (of whichever sort) C2Cyl(D)C\to 2Cyl(D), where the objects of 2Cyl(D)2Cyl(D) are the 2-cells of DD, and so on. Therefore, CC' classifies not only pseudofunctors out of CC, but transformations and modifications between them; thus we have an isomorphism

[C op,Cat][(C) op,Cat] strict,pseudo[C^{op},Cat] \cong [(C')^{op},Cat]_{strict,pseudo}

where [A,B] strict,pseudo[A,B]_{strict,pseudo} denotes the 2-category of strict 2-functors, pseudonatural transformations, and modifications between two strict 2-categories. Thus we can equally well analyze the functor

[(C) op,Cat] strict,pseudo(C(,x)¯,F¯)F¯(x)=F(x) [(C')^{op},Cat]_{strict,pseudo}(\overline{C(-,x)}, \overline{F}) \to \overline{F}(x) = F(x)

given by evaluation at 1 x1_x. Here C(,x)¯\overline{C(-,x)} and F¯\overline{F} denote the strict 2-functors (C) opCat(C')^{op}\to Cat corresponding to the pseudofunctors C(,x)C(-,x) and FF under the ()(-)' adjunction. However, we also have a strict 2-functor C(,x)C'(-,x), and the equivalence CCC\simeq C' induces an equivalence C(,x)C(,x)¯C'(-,x)\simeq \overline{C(-,x)}. Therefore, it suffices to analyze the functor

[(C) op,Cat] strict,pseudo(C(,x),F¯)F¯(x). [(C')^{op},Cat]_{strict,pseudo}(C'(-,x), \overline{F}) \to \overline{F}(x).

Now for any AA and BB, we have an inclusion functor [A,B] strict,strict[A,B] strict,pseudo[A,B]_{strict,strict} \to [A,B]_{strict,pseudo} where [A,B] strict,strict[A,B]_{strict,strict} denotes the 2-category of strict 2-functors, strict 2-natural transformations, and modifications. This functor is bijective on objects and locally fully faithful. Moreover, the composite

[(C) op,Cat] strict,strict(C(,x),F¯)[(C) op,Cat] strict,pseudo(C(,x),F¯)F¯(x). [(C')^{op},Cat]_{strict,strict}(C'(-,x), \overline{F}) \to [(C')^{op},Cat]_{strict,pseudo}(C'(-,x), \overline{F}) \to \overline{F}(x).

is an isomorphism, by the enriched Yoneda lemma, in the special case of CatCat-enrichment. Since

[(C) op,Cat] strict,strict(C(,x),F¯)[(C) op,Cat] strict,pseudo(C(,x),F¯)[(C')^{op},Cat]_{strict,strict}(C'(-,x), \overline{F}) \to [(C')^{op},Cat]_{strict,pseudo}(C'(-,x), \overline{F})

is fully faithful, if we can show that it is essentially surjective, then the 2-out-of-3 property for equivalences of categories will imply that the desired functor is an equivalence.

Here we at last descend to something concrete. Given α:C(,x)F¯\alpha\colon C'(-,x)\to \overline{F}, we have an obvious choice for a strict transformation for it to be equivalent to, namely β\beta whose components β y:C(y,x)F¯(y)\beta_y\colon C'(y,x)\to \overline{F}(y) is given by fF¯(f)(a)f \mapsto \overline{F}(f)(a) where a=α x(1 x)F¯(x)a = \alpha_x(1_x)\in \overline{F}(x). Since α\alpha is pseudonatural, for any f:yxf\colon y\to x in CC' we have an isomorphism

α y(f)=α y(f1 x)F¯(f)(α x(1 x))=F¯(f)(a)=β y(f).\alpha_y(f) = \alpha_y(f\circ 1_x) \cong \overline{F}(f)(\alpha_x(1_x)) = \overline{F}(f)(a) = \beta_y(f).

We then simply verify that these isomorphisms are the components of an (invertible) modification αβ\alpha\cong \beta. This completes the proof.


A treatment of the bicategorical Yoneda embedding and lemma is in Chap. 8 of

An account of Morita equivalence as a corollary of the Yoneda lemma for bicategories is in

Last revised on April 23, 2020 at 05:29:41. See the history of this page for a list of all contributions to it.