Lack's coherence theorem

One form of the coherence theorem for bicategories states that every bicategory is equivalent to a strict 2-category. Lack’s coherence theorem (named for Steve Lack) states that every naturally-occurring bicategory is equivalent to a naturally occurring strict 2-category. Obviously this is not a theorem in the usual sense, but rather an observation about a number of similar examples.

Instances of Lack’s coherence theorem include: