Documentation

Mathlib.Tactic.CategoryTheory.Coherence.Normalize

Normalization of 2-morphisms in bicategories #

This file provides a function that normalizes 2-morphisms in bicategories. The function also used to normalize morphisms in monoidal categories. This is used in the string diagram widget given in Mathlib.Tactic.StringDiagram, as well as monoidal and bicategory tactics.

We say that the 2-morphism η in a bicategory is in normal form if

  1. η is of the form α₀ ≫ η₀ ≫ α₁ ≫ η₁ ≫ ... αₘ ≫ ηₘ ≫ αₘ₊₁ where each αᵢ is a structural 2-morphism (consisting of associators and unitors),
  2. each ηᵢ is a non-structural 2-morphism of the form f₁ ◁ ... ◁ fₙ ◁ θ, and
  3. θ is of the form ι₁ ◫ ... ◫ ιₗ, and
  4. each ιᵢ is of the form κ ▷ g₁ ▷ ... ▷ gₖ.

Note that the horizontal composition ◫ is not currently defined for bicategories. In the monoidal category setting, the horizontal composition is defined as the tensorHom, denoted by ⊗.

Note that the structural morphisms αᵢ are not necessarily normalized, as the main purpose is to get a list of the non-structural morphisms out.

Currently, the primary application of the normalization tactic in mind is drawing string diagrams, which are graphical representations of morphisms in monoidal categories, in the infoview. When drawing string diagrams, we often ignore associators and unitors (i.e., drawing morphisms in strict monoidal categories). On the other hand, in Lean, it is considered difficult to formalize the concept of strict monoidal categories due to the feature of dependent type theory. The normalization tactic can remove associators and unitors from the expression, extracting the necessary data for drawing string diagrams.

The string diagrams widget is to use Penrose (https://github.com/penrose) via ProofWidget. However, it should be noted that the normalization procedure in this file does not rely on specific settings, allowing for broader application. Future plans include the following. At least I (Yuma) would like to work on these in the future, but it might not be immediate. If anyone is interested, I would be happy to discuss.

Main definitions #

source
inductive Mathlib.Tactic.BicategoryLike.WhiskerRight :
Type

Expressions of the form η ▷ f₁ ▷ ... ▷ fₙ.

Instances For
source
instance Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerRight :
Inhabited Mathlib.Tactic.BicategoryLike.WhiskerRight
Equations
source
def Mathlib.Tactic.BicategoryLike.WhiskerRight.e :
Mathlib.Tactic.BicategoryLike.WhiskerRight → Mathlib.Tactic.BicategoryLike.Mor₂

The underlying Mor₂ term of a WhiskerRight term.

Equations
source
inductive Mathlib.Tactic.BicategoryLike.HorizontalComp :
Type

Expressions of the form η₁ ⊗ ... ⊗ ηₙ.

Instances For
source
instance Mathlib.Tactic.BicategoryLike.instInhabitedHorizontalComp :
Inhabited Mathlib.Tactic.BicategoryLike.HorizontalComp
Equations
source
def Mathlib.Tactic.BicategoryLike.HorizontalComp.e :
Mathlib.Tactic.BicategoryLike.HorizontalComp → Mathlib.Tactic.BicategoryLike.Mor₂

The underlying Mor₂ term of a HorizontalComp term.

Equations
source
inductive Mathlib.Tactic.BicategoryLike.WhiskerLeft :
Type

Expressions of the form f₁ ◁ ... ◁ fₙ ◁ η.

Instances For
source
instance Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerLeft :
Inhabited Mathlib.Tactic.BicategoryLike.WhiskerLeft
Equations
source
def Mathlib.Tactic.BicategoryLike.WhiskerLeft.e :
Mathlib.Tactic.BicategoryLike.WhiskerLeft → Mathlib.Tactic.BicategoryLike.Mor₂

The underlying Mor₂ term of a WhiskerLeft term.

Equations
source
def Mathlib.Tactic.BicategoryLike.Mor₂Iso.isStructural (α : Mathlib.Tactic.BicategoryLike.Mor₂Iso) :
Bool

Whether a given 2-isomorphism is structural or not.

Equations
source
@[reducible, inline]
abbrev Mathlib.Tactic.BicategoryLike.Structural :
Type

Expressions for structural isomorphisms. We do not impose the condition isStructural since it is not needed to write the tactic.

Equations
source
inductive Mathlib.Tactic.BicategoryLike.NormalExpr :
Type

Normalized expressions for 2-morphisms.

Instances For
source
instance Mathlib.Tactic.BicategoryLike.instInhabitedNormalExpr :
Inhabited Mathlib.Tactic.BicategoryLike.NormalExpr
Equations
source
def Mathlib.Tactic.BicategoryLike.NormalExpr.e :
Mathlib.Tactic.BicategoryLike.NormalExpr → Mathlib.Tactic.BicategoryLike.Mor₂

The underlying Mor₂ term of a NormalExpr term.

Equations
source
class Mathlib.Tactic.BicategoryLike.MonadWhiskerRight (m : Type → Type) :
Type

A monad equipped with the ability to construct WhiskerRight terms.

Instances
    source
    class Mathlib.Tactic.BicategoryLike.MonadHorizontalComp (m : Type → Type) extends Mathlib.Tactic.BicategoryLike.MonadWhiskerRight :
    Type

    A monad equipped with the ability to construct HorizontalComp terms.

    Instances
      source
      class Mathlib.Tactic.BicategoryLike.MonadWhiskerLeft (m : Type → Type) extends Mathlib.Tactic.BicategoryLike.MonadHorizontalComp :
      Type

      A monad equipped with the ability to construct WhiskerLeft terms.

      Instances
        source
        class Mathlib.Tactic.BicategoryLike.MonadNormalExpr (m : Type → Type) extends Mathlib.Tactic.BicategoryLike.MonadWhiskerLeft :
        Type

        A monad equipped with the ability to construct NormalExpr terms.

        Instances
        source
        def Mathlib.Tactic.BicategoryLike.WhiskerRight.srcM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] :
        Mathlib.Tactic.BicategoryLike.WhiskerRight → m Mathlib.Tactic.BicategoryLike.Mor₁

        The domain of a 2-morphism.

        Equations
        source
        def Mathlib.Tactic.BicategoryLike.WhiskerRight.tgtM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] :
        Mathlib.Tactic.BicategoryLike.WhiskerRight → m Mathlib.Tactic.BicategoryLike.Mor₁

        The codomain of a 2-morphism.

        Equations
        source
        def Mathlib.Tactic.BicategoryLike.HorizontalComp.srcM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] :
        Mathlib.Tactic.BicategoryLike.HorizontalComp → m Mathlib.Tactic.BicategoryLike.Mor₁

        The domain of a 2-morphism.

        Equations
        source
        def Mathlib.Tactic.BicategoryLike.HorizontalComp.tgtM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] :
        Mathlib.Tactic.BicategoryLike.HorizontalComp → m Mathlib.Tactic.BicategoryLike.Mor₁

        The codomain of a 2-morphism.

        Equations
        source
        def Mathlib.Tactic.BicategoryLike.WhiskerLeft.srcM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] :
        Mathlib.Tactic.BicategoryLike.WhiskerLeft → m Mathlib.Tactic.BicategoryLike.Mor₁

        The domain of a 2-morphism.

        Equations
        source
        def Mathlib.Tactic.BicategoryLike.WhiskerLeft.tgtM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] :
        Mathlib.Tactic.BicategoryLike.WhiskerLeft → m Mathlib.Tactic.BicategoryLike.Mor₁

        The codomain of a 2-morphism.

        Equations
        source
        def Mathlib.Tactic.BicategoryLike.NormalExpr.srcM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] :
        Mathlib.Tactic.BicategoryLike.NormalExpr → m Mathlib.Tactic.BicategoryLike.Mor₁

        The domain of a 2-morphism.

        Equations
        source
        def Mathlib.Tactic.BicategoryLike.NormalExpr.tgtM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] :
        Mathlib.Tactic.BicategoryLike.NormalExpr → m Mathlib.Tactic.BicategoryLike.Mor₁

        The codomain of a 2-morphism.

        Equations
        source
        def Mathlib.Tactic.BicategoryLike.NormalExpr.idM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] (f : Mathlib.Tactic.BicategoryLike.Mor₁) :
        m Mathlib.Tactic.BicategoryLike.NormalExpr

        The identity 2-morphism as a term of normalExpr.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Mathlib.Tactic.BicategoryLike.NormalExpr.associatorM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] (f : Mathlib.Tactic.BicategoryLike.Mor₁) (g : Mathlib.Tactic.BicategoryLike.Mor₁) (h : Mathlib.Tactic.BicategoryLike.Mor₁) :
        m Mathlib.Tactic.BicategoryLike.NormalExpr

        The associator as a term of normalExpr.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Mathlib.Tactic.BicategoryLike.NormalExpr.associatorInvM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] (f : Mathlib.Tactic.BicategoryLike.Mor₁) (g : Mathlib.Tactic.BicategoryLike.Mor₁) (h : Mathlib.Tactic.BicategoryLike.Mor₁) :
        m Mathlib.Tactic.BicategoryLike.NormalExpr

        The inverse of the associator as a term of normalExpr.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Mathlib.Tactic.BicategoryLike.NormalExpr.leftUnitorM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] (f : Mathlib.Tactic.BicategoryLike.Mor₁) :
        m Mathlib.Tactic.BicategoryLike.NormalExpr

        The left unitor as a term of normalExpr.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Mathlib.Tactic.BicategoryLike.NormalExpr.leftUnitorInvM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] (f : Mathlib.Tactic.BicategoryLike.Mor₁) :
        m Mathlib.Tactic.BicategoryLike.NormalExpr

        The inverse of the left unitor as a term of normalExpr.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Mathlib.Tactic.BicategoryLike.NormalExpr.rightUnitorM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] (f : Mathlib.Tactic.BicategoryLike.Mor₁) :
        m Mathlib.Tactic.BicategoryLike.NormalExpr

        The right unitor as a term of normalExpr.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Mathlib.Tactic.BicategoryLike.NormalExpr.rightUnitorInvM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] (f : Mathlib.Tactic.BicategoryLike.Mor₁) :
        m Mathlib.Tactic.BicategoryLike.NormalExpr

        The inverse of the right unitor as a term of normalExpr.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Mathlib.Tactic.BicategoryLike.NormalExpr.ofM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] (η : Mathlib.Tactic.BicategoryLike.WhiskerLeft) :
        m Mathlib.Tactic.BicategoryLike.NormalExpr

        Construct a NormalExpr expression from a WhiskerLeft expression.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Mathlib.Tactic.BicategoryLike.NormalExpr.ofAtomM {m : Type → Type} [Monad m] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] (η : Mathlib.Tactic.BicategoryLike.Atom) :
        m Mathlib.Tactic.BicategoryLike.NormalExpr

        Construct a NormalExpr expression from a Lean expression for an atomic 2-morphism.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Mathlib.Tactic.BicategoryLike.NormalExpr.toList :
        Mathlib.Tactic.BicategoryLike.NormalExpr → List Mathlib.Tactic.BicategoryLike.WhiskerLeft

        Convert a NormalExpr expression into a list of WhiskerLeft expressions.

        Equations
        source
        structure Mathlib.Tactic.BicategoryLike.Eval.Result :
        Type

        The result of evaluating an expression into normal form.

        Instances For
        source
        instance Mathlib.Tactic.BicategoryLike.Eval.instInhabitedResult :
        Inhabited Mathlib.Tactic.BicategoryLike.Eval.Result
        Equations
        source
        class Mathlib.Tactic.BicategoryLike.MkEvalComp (m : Type → Type) :
        Type

        Evaluate the expression α ≫ β.

        Instances
        source
        class Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft (m : Type → Type) :
        Type

        Evaluatte the expression f ◁ η.

        Instances
        source
        class Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight (m : Type → Type) :
        Type

        Evaluate the expression η ▷ f.

        Instances
        source
        class Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp (m : Type → Type) :
        Type

        Evaluate the expression η ◫ θ.

        Instances
        source
        class Mathlib.Tactic.BicategoryLike.MkEval (m : Type → Type) extends Mathlib.Tactic.BicategoryLike.MkEvalComp , Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft , Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight , Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp :
        Type

        Evaluate the expression of a 2-morphism into a normalized form.

        Instances
        source
        def Mathlib.Tactic.BicategoryLike.evalCompNil {ρ : Type} [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] (α : Mathlib.Tactic.BicategoryLike.Structural) :
        Mathlib.Tactic.BicategoryLike.NormalExpr → Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result

        Evaluate the expression α ≫ η into a normalized form.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Mathlib.Tactic.BicategoryLike.evalComp {ρ : Type} [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] :
        Mathlib.Tactic.BicategoryLike.NormalExpr → Mathlib.Tactic.BicategoryLike.NormalExpr → Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result

        Evaluate the expression η ≫ θ into a normalized form.

        Equations
        source
        @[irreducible]
        def Mathlib.Tactic.BicategoryLike.evalWhiskerLeft {ρ : Type} [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] :
        Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.NormalExpr → Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result

        Evaluate the expression f ◁ η into a normalized form.

        source
        partial def Mathlib.Tactic.BicategoryLike.evalWhiskerRightAux {ρ : Type} [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] :
        Mathlib.Tactic.BicategoryLike.HorizontalComp → Mathlib.Tactic.BicategoryLike.Atom₁ → Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result

        Evaluate the expression η ▷ f into a normalized form.

        source
        partial def Mathlib.Tactic.BicategoryLike.evalWhiskerRight {ρ : Type} [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] :
        Mathlib.Tactic.BicategoryLike.NormalExpr → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result

        Evaluate the expression η ▷ f into a normalized form.

        source
        partial def Mathlib.Tactic.BicategoryLike.evalHorizontalCompAux {ρ : Type} [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] :
        Mathlib.Tactic.BicategoryLike.HorizontalComp → Mathlib.Tactic.BicategoryLike.HorizontalComp → Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result

        Evaluate the expression η ⊗ θ into a normalized form.

        source
        partial def Mathlib.Tactic.BicategoryLike.evalHorizontalCompAux' {ρ : Type} [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] :
        Mathlib.Tactic.BicategoryLike.WhiskerLeft → Mathlib.Tactic.BicategoryLike.WhiskerLeft → Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result

        Evaluate the expression η ⊗ θ into a normalized form.

        source
        partial def Mathlib.Tactic.BicategoryLike.evalHorizontalComp {ρ : Type} [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] :
        Mathlib.Tactic.BicategoryLike.NormalExpr → Mathlib.Tactic.BicategoryLike.NormalExpr → Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result

        Evaluate the expression η ⊗ θ into a normalized form.

        source
        def Mathlib.Tactic.BicategoryLike.traceProof {ρ : Type} (nm : Lean.Name) (result : Lean.Expr) :
        Mathlib.Tactic.BicategoryLike.CoherenceM ρ Unit

        Trace the proof of the normalization.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Mathlib.Tactic.BicategoryLike.eval {ρ : Type} [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadNormalExpr (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MkEval (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] [Mathlib.Tactic.BicategoryLike.MonadMor₂ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] (nm : Lean.Name) (e : Mathlib.Tactic.BicategoryLike.Mor₂) :
        Mathlib.Tactic.BicategoryLike.CoherenceM ρ Mathlib.Tactic.BicategoryLike.Eval.Result

        Evaluate the expression of a 2-morphism into a normalized form.