The tricategory of formal composites and its strictification

Understand

The results of this thesis allows one to replace calculations in tricategories with equivalent calculations in Gray categories (aka semistrict tricategories).

• In particular the rewriting calculus for Gray categories as used for example by the online proof assistant globular (arXiv:1612.01093), or equivalently the Gray-diagrams of arXiv:1211.0529 can then be used also in the case of a fully weak tricategory.