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 , any object , and any pseudofunctor , there is an equivalence of categories
which is pseudonatural in and , and which is given by evaluation at , i.e. maps to .
In particular, the Yoneda lemma for bicategories implies that there is a Yoneda embedding for bicategories which is 2-fully-faithful?, i.e. an equivalence on hom-categories. Therefore, is equivalent to a sub-bicategory of . Since Cat is a strict 2-category, it follows that 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 seems to be hard to find in the literature. (Anyone have references to add?)
We will take it for granted that 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 ” functor
is well-defined and pseudonatural in and ; 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 pseudoalegbras?, which says that for a suitably well-behaved strict 2-monad , the inclusion --- of the 2-category of strict -algebras and strict -morphisms into the 2-category of pseudo -algebras and pseudo -morphisms has a left adjoint, usually written as . Moreover, for any pseudo -algebra , the unit is an equivalence in --.
First, there is a 2-monad such that strict -algebras are strict 2-categories, strict -morphisms are strict 2-functors, pseudo -algebras are unbiased bicategories?, and pseudo -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 is a strict 2-category, for any bicategory there is a strict 2-category such that pseudofunctors are in bijection with strict 2-functors .
Now note that a pseudonatural transformation between two pseudofunctors (resp. strict 2-functors) is the same as a single pseudofunctor (resp. strict 2-functor) , where is the bicategory whose objects are the 1-cells of , whose 1-cells are squares in commuting up to isomorphism, and whose 2-cells are “cylinders” in . Likewise, a modification between two such transformations is the same as a single functor (of whichever sort) , where the objects of are the 2-cells of , and so on. Therefore, classifies not only pseudofunctors out of , but transformations and modifications between them; thus we have an isomorphism
where 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
given by evaluation at . Here and denote the strict 2-functors corresponding to the pseudofunctors and under the adjunction. However, we also have a strict 2-functor , and the equivalence induces an equivalence . Therefore, it suffices to analyze the functor
Now for any and , we have an inclusion functor where 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
is an isomorphism, by the Yoneda lemma for enriched categories?, in the special case of -enrichment. Since
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 , we have an obvious choice for a strict transformation for it to be equivalent to, namely whose components is given by where . Since is pseudonatural, for any in we have an isomorphism
We then simply verify that these isomorphisms are the components of an (invertible) modification . This completes the proof.