mathlib3 documentation


The coherence theorem for bicategories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file, we prove the coherence theorem for bicategories, stated in the following form: the free bicategory over any quiver is locally thin.

The proof is almost the same as the proof of the coherence theorem for monoidal categories that has been previously formalized in mathlib, which is based on the proof described by Ilya Beylin and Peter Dybjer. The idea is to view a path on a quiver as a normal form of a 1-morphism in the free bicategory on the same quiver. A normalization procedure is then described by normalize : pseudofunctor (free_bicategory B) (locally_discrete (paths B)), which is a pseudofunctor from the free bicategory to the locally discrete bicategory on the path category. It turns out that this pseudofunctor is locally an equivalence of categories, and the coherence theorem follows immediately from this fact.

Main statements #

References #

The inclusion from the locally discrete bicategory on the path category into the free bicategory as a prelax functor. This will be promoted to a pseudofunctor after proving the coherence theorem. See inclusion.


The normalization of the composition of p : path a b and f : hom b c. p will eventually be taken to be nil and we then get the normalization of f alone, but the auxiliary p is necessary for Lean to accept the definition of normalize_iso and the whisker_left case of normalize_aux_congr and normalize_naturality.


Given a 2-morphism between f and g in the free bicategory, we have the equality normalize_aux p f = normalize_aux p g.

@[protected, instance]

The coherence theorem for bicategories.