10 - Coherence via free constructions

Summary

In this chapter, we will prove a coherence theorem comparing free tricategories to free Gray-categories. This theorem states that the natural functor induced by the universal property from the free tricategory to the free Gray-category on the same underlying data is a triequivalence. It is also a simple matter to prove a similar result comparing Gray-categories and strict 3-categories: the natural functor induced by the universal property from the free Gray-category to the free strict 3-category on the same underlying data is a triequivalence. This latter result might seem surprising, as it is well-known that not every tricategory is triequivalent to a strict 3-category, but in fact these results only express that the maps of monads from the free tricategory monad to the free Gray-category monad to the free strict 3-category monad can be equipped with contractions in the sense of Leinster (2004); this condition is one requirement for a monad to be a reasonable monad for a theory of weak 3-categories. As in the case of the coherence theory for bicategories, we can use this result to prove that diagrams of constraint 3-cells of a certain type always commute. Our results differ from the analogous ones for bicategories in that only some diagrams commute for tricategories but all diagrams of constraint 2-cells commute in a bicategory. As an example, we explicitly construct a diagram of constraint 3-cells that is not required to commute in general, and in fact does not commute in example tricategories which arise from braided monoidal categories.