Documentation

Mathlib.CategoryTheory.Bicategory.Coherence

The coherence theorem for bicategories #

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 (FreeBicategory B) (LocallyDiscrete (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 #

Category structure on Hom a b. In this file, we will use Hom a b for a b : B (precisely, FreeBicategory.Hom a b) instead of the definitionally equal expression a ⟶ b for a b : FreeBicategory B. The main reason is that we have to annoyingly write @Quiver.Hom (FreeBicategory B) _ a b to get the latter expression when given a b : B.

Equations
Instances For

    The discrete category on the paths includes into the category of 1-morphisms in the free bicategory.

    Equations
    Instances For

      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.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        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 normalizeIso and the whisker_left case of normalizeAux_congr and normalize_naturality.

        Equations
        Instances For

          A 2-isomorphism between a partially-normalized 1-morphism in the free bicategory to the fully-normalized 1-morphism.

          Equations
          Instances For

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

            The normalization pseudofunctor for the free bicategory on a quiver B.

            Instances For

              Auxiliary definition for normalizeEquiv.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                Normalization as an equivalence of categories.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  The coherence theorem for bicategories.

                  Equations
                  • =

                  Auxiliary definition for inclusion.

                  Equations
                  Instances For

                    The inclusion pseudofunctor from the locally discrete bicategory on the path category into the free bicategory.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For