nLab
coherence theorem for bicategories with finite limits

Theorem

Theorem

(Power) Any bicategory with finite bilimits is equivalent to a strict 2-category with finite flexible limits.

Proof

Let $K$ be a bicategory with finite bilimits, let $K\hookrightarrow [K^{\mathrm{op}},\mathrm{Cat}]$ be its Yoneda embedding, and let $K\prime$ be the closure of $K$ in $[K^{\mathrm{op}},\mathrm{Cat}]$ under finite flexible limits. Since $\mathrm{Cat}$ is a strict 2-category with finite flexible limits, so is $[K^{\mathrm{op}},\mathrm{Cat}]$. And since $K$ has finite bilimits, and these are preserved by its Yoneda embedding, while flexible limits are in particular bilimits, every object of $K\prime$ is equivalent to an object of $K$. Thus, $K\simeq K\prime$.

References

• John Power, “Coherence for bicategories with finite bilimits”, Categories in computer science and logic, 1989.