# On the coherence theorem for bicategories

The coherence theorem for bicategories, as usually stated, reads

Any bicategory $B$ is biequivalent to a (strict) 2-category.

It is possible to give an explicit construction of the strictification as the full image of its Yoneda embedding $y:B\rightarrow [B,\text{Cat}]$, see for instance this reference.

This seems like a natural construction, so I would expect an equivalence of tricategories

$$\text{Bicat} \leftrightarrows 2\text{-Cat}$$

where the rightgoing functor is the full image of the yoneda embedding, and the leftgoing functor is the inclusion. However, I cannot find such a statement in the literature. If it is true, a reference would be appreciated.

• If you want a quick overview of the situation, you could try the slides here, especially pages 8 and 14: maths.ed.ac.uk/~tl/toronto – Tom Leinster Mar 2 '15 at 14:06

Probably you had some trouble finding this because the search term $2$-$\text{Cat}$ is not accurate enough; you want not the cartesian monoidal product on $2$-$\text{Cat}$, but rather what is called the Gray monoidal product; the tricategory you want then is denoted $\text{Gray}$, the tricategory of strict 2-categories, strict 2-functors, pseudonatural transformations, and modifications between them, but most usefully considered as equipped with the Gray tensor product.