Documentation

Mathlib.Tactic.CategoryTheory.BicategoryCoherence

A coherence tactic for bicategories #

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.

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)

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

  • 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.

Instances
    Equations
    @[instance 100]
    Equations

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

    Instances

      Helper function for throwing exceptions.

      Equations
      Instances For

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

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

          Auxiliary definition for bicategorical_coherence.

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

            Coherence tactic for bicategories.

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

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

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

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

                Equations
                • One or more equations did not get rendered due to their size.
                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.