Documentation

Mathlib.Tactic.CategoryTheory.BicategoryCoherence

A coherence tactic for bicategories, and ⊗≫ (composition up to associators) #

We provide a bicategory_coherence tactic, which proves that any two 2-morphisms (with the same source and target) in a bicategory which are built out of associators and unitors are equal.

We also provide f ⊗≫ g, the bicategoricalComp operation, which automatically inserts associators and unitors as needed to make the target of f match the source of g.

This file mainly deals with the type class setup for the coherence tactic. The actual front end tactic is given in Mathlib.Tactic.CategoryTheory.Coherence at the same time as the coherence tactic for monoidal categories.

class Mathlib.Tactic.BicategoryCoherence.LiftHom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a b) :
Type (max u v)
  • lift : CategoryTheory.FreeBicategory.of.obj a CategoryTheory.FreeBicategory.of.obj b

    A lift of a morphism to the free bicategory. This should only exist for "structural" morphisms.

A typeclass carrying a choice of lift of a 1-morphism from B to FreeBicategory B.

Instances

    A typeclass carrying a choice of lift of a 2-morphism from B to FreeBicategory B.

    Instances
      • hom' : f g

        The chosen structural isomorphism between to 1-morphisms.

      • isIso : CategoryTheory.IsIso Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom'

      A typeclass carrying a choice of bicategorical structural isomorphism between two objects. Used by the ⊗≫ bicategorical composition operator, and the coherence tactic.

      Instances
        @[simp]
        theorem Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.refl_hom' {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a b) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] :
        Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom' = CategoryTheory.CategoryStruct.id f

        Construct an isomorphism between two objects in a bicategorical category out of unitors and associators.

        Instances For

          Compose two morphisms in a bicategorical category, inserting unitors and associators between as necessary.

          Instances For

            Compose two morphisms in a bicategorical category, inserting unitors and associators between as necessary.

            Instances For

              Compose two isomorphisms in a bicategorical category, inserting unitors and associators between as necessary.

              Instances For

                Compose two isomorphisms in a bicategorical category, inserting unitors and associators between as necessary.

                Instances For

                  Helper function for throwing exceptions.

                  Instances For

                    Helper function for throwing exceptions with respect to the main goal.

                    Instances For

                      Auxiliary definition for bicategorical_coherence.

                      Instances For

                        Coherence tactic for bicategories. Use pure_coherence instead, which is a frontend to this one.

                        Instances For

                          Simp lemmas for rewriting a 2-morphism into a normal form.

                          Instances For

                            Auxiliary simp lemma for the coherence tactic: this move brackets to the left in order to expose a maximal prefix built out of unitors and associators.