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.lean, 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.

• Currently, the string diagrams widget only do drawing. It would be better they also generate proofs. That is, by manipulating the string diagrams displayed in the infoview with a mouse to generate proofs. In https://github.com/leanprover-community/mathlib4/pull/10581, the string diagram widget only uses the morphisms generated by the normalization tactic and does not use proof terms ensuring that the original morphism and the normalized morphism are equal. Proof terms will be necessary for proof generation.

• There is also the possibility of using homotopy.io (https://github.com/homotopy-io), a graphical proof assistant for category theory, from Lean. At this point, I have very few ideas regarding this approach.

Main definitions

• Tactic.BicategoryLike.eval: Given a Lean expression e that represents a morphism in a monoidal category, this function returns a pair of ⟨e', pf⟩ where e' is the normalized expression of e and pf is a proof that e = e'.

inductive Mathlib.Tactic.BicategoryLike.WhiskerRight : Type

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

• of (η : Atom) : WhiskerRight

  Construct the expression for an atomic 2-morphism.

• whisker (e : Mor₂) (η : WhiskerRight) (f : Atom₁) : WhiskerRight

  Construct the expression for η ▷ f.

instance Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerRight : Inhabited WhiskerRight

Equations

• Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerRight = { default := Mathlib.Tactic.BicategoryLike.WhiskerRight.of default }

def Mathlib.Tactic.BicategoryLike.WhiskerRight.e : WhiskerRight → Mor₂

The underlying Mor₂ term of a WhiskerRight term.

Equations

• (Mathlib.Tactic.BicategoryLike.WhiskerRight.of η).e = Mathlib.Tactic.BicategoryLike.Mor₂.of η
• (Mathlib.Tactic.BicategoryLike.WhiskerRight.whisker e η f).e = e

inductive Mathlib.Tactic.BicategoryLike.HorizontalComp : Type

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

• of (η : WhiskerRight) : HorizontalComp
• cons (e : Mor₂) (η : WhiskerRight) (ηs : HorizontalComp) : HorizontalComp

instance Mathlib.Tactic.BicategoryLike.instInhabitedHorizontalComp : Inhabited HorizontalComp

Equations

• Mathlib.Tactic.BicategoryLike.instInhabitedHorizontalComp = { default := Mathlib.Tactic.BicategoryLike.HorizontalComp.of default }

def Mathlib.Tactic.BicategoryLike.HorizontalComp.e : HorizontalComp → Mor₂

The underlying Mor₂ term of a HorizontalComp term.

Equations

• (Mathlib.Tactic.BicategoryLike.HorizontalComp.of η).e = η.e
• (Mathlib.Tactic.BicategoryLike.HorizontalComp.cons e η ηs).e = e

inductive Mathlib.Tactic.BicategoryLike.WhiskerLeft : Type

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

• of (η : HorizontalComp) : WhiskerLeft

  Construct the expression for a right-whiskered 2-morphism.

• whisker (e : Mor₂) (f : Atom₁) (η : WhiskerLeft) : WhiskerLeft

  Construct the expression for f ◁ η.

instance Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerLeft : Inhabited WhiskerLeft

Equations

• Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerLeft = { default := Mathlib.Tactic.BicategoryLike.WhiskerLeft.of default }

def Mathlib.Tactic.BicategoryLike.WhiskerLeft.e : WhiskerLeft → Mor₂

The underlying Mor₂ term of a WhiskerLeft term.

Equations

• (Mathlib.Tactic.BicategoryLike.WhiskerLeft.of η).e = η.e
• (Mathlib.Tactic.BicategoryLike.WhiskerLeft.whisker e f η).e = e

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

Whether a given 2-isomorphism is structural or not.

Equations

• (Mathlib.Tactic.BicategoryLike.Mor₂Iso.structuralAtom α_2).isStructural = true
• (Mathlib.Tactic.BicategoryLike.Mor₂Iso.comp e f g h η θ).isStructural = (η.isStructural && θ.isStructural)
• (Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerLeft e f g h η).isStructural = η.isStructural
• (Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerRight e f g η h).isStructural = η.isStructural
• (Mathlib.Tactic.BicategoryLike.Mor₂Iso.horizontalComp e f₁ g₁ f₂ g₂ η θ).isStructural = (η.isStructural && θ.isStructural)
• (Mathlib.Tactic.BicategoryLike.Mor₂Iso.inv e f g η).isStructural = η.isStructural
• (Mathlib.Tactic.BicategoryLike.Mor₂Iso.coherenceComp e f g h i α_2 η θ).isStructural = (η.isStructural && θ.isStructural)
• (Mathlib.Tactic.BicategoryLike.Mor₂Iso.of η).isStructural = false

@[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

• Mathlib.Tactic.BicategoryLike.Structural = Mathlib.Tactic.BicategoryLike.Mor₂Iso

inductive Mathlib.Tactic.BicategoryLike.NormalExpr : Type

Normalized expressions for 2-morphisms.

• nil (e : Mor₂) (α : Structural) : NormalExpr

  Construct the expression for a structural 2-morphism.

• cons (e : Mor₂) (α : Structural) (η : WhiskerLeft) (ηs : NormalExpr) : NormalExpr

  Construct the normalized expression of a 2-morphism α ≫ η ≫ ηs recursively.

instance Mathlib.Tactic.BicategoryLike.instInhabitedNormalExpr : Inhabited NormalExpr

Equations

• Mathlib.Tactic.BicategoryLike.instInhabitedNormalExpr = { default := Mathlib.Tactic.BicategoryLike.NormalExpr.nil default default }

def Mathlib.Tactic.BicategoryLike.NormalExpr.e : NormalExpr → Mor₂

The underlying Mor₂ term of a NormalExpr term.

Equations

• (Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α).e = e
• (Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs).e = e

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

A monad equipped with the ability to construct WhiskerRight terms.

• whiskerRightM (η : WhiskerRight) (f : Atom₁) : m WhiskerRight

  The expression for the right whiskering η ▷ f.

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

A monad equipped with the ability to construct HorizontalComp terms.

• whiskerRightM (η : WhiskerRight) (f : Atom₁) : m WhiskerRight
• hConsM (η : WhiskerRight) (ηs : HorizontalComp) : m HorizontalComp

  The expression for the horizontal composition η ◫ ηs.

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

A monad equipped with the ability to construct WhiskerLeft terms.

• whiskerRightM (η : WhiskerRight) (f : Atom₁) : m WhiskerRight
• hConsM (η : WhiskerRight) (ηs : HorizontalComp) : m HorizontalComp
• whiskerLeftM (f : Atom₁) (η : WhiskerLeft) : m WhiskerLeft

  The expression for the left whiskering f ▷ η.

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

A monad equipped with the ability to construct NormalExpr terms.

• whiskerRightM (η : WhiskerRight) (f : Atom₁) : m WhiskerRight
• hConsM (η : WhiskerRight) (ηs : HorizontalComp) : m HorizontalComp
• whiskerLeftM (f : Atom₁) (η : WhiskerLeft) : m WhiskerLeft
• nilM (α : Structural) : m NormalExpr

  The expression for the structural 2-morphism α.

• consM (headStructural : Structural) (η : WhiskerLeft) (ηs : NormalExpr) : m NormalExpr

  The expression for the normalized 2-morphism α ≫ η ≫ ηs.

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

The domain of a 2-morphism.

Equations

• (Mathlib.Tactic.BicategoryLike.WhiskerRight.of η).srcM = pure η.src
• (Mathlib.Tactic.BicategoryLike.WhiskerRight.whisker e η f).srcM = do let __do_lift ← η.srcM Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M __do_lift (Mathlib.Tactic.BicategoryLike.Mor₁.of f)

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

The codomain of a 2-morphism.

Equations

• (Mathlib.Tactic.BicategoryLike.WhiskerRight.of η).tgtM = pure η.tgt
• (Mathlib.Tactic.BicategoryLike.WhiskerRight.whisker e η f).tgtM = do let __do_lift ← η.tgtM Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M __do_lift (Mathlib.Tactic.BicategoryLike.Mor₁.of f)

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

The domain of a 2-morphism.

Equations

• (Mathlib.Tactic.BicategoryLike.HorizontalComp.of η).srcM = η.srcM
• (Mathlib.Tactic.BicategoryLike.HorizontalComp.cons e η ηs).srcM = do let __do_lift ← η.srcM let __do_lift_1 ← ηs.srcM Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M __do_lift __do_lift_1

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

The codomain of a 2-morphism.

Equations

• (Mathlib.Tactic.BicategoryLike.HorizontalComp.of η).tgtM = η.tgtM
• (Mathlib.Tactic.BicategoryLike.HorizontalComp.cons e η ηs).tgtM = do let __do_lift ← η.tgtM let __do_lift_1 ← ηs.tgtM Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M __do_lift __do_lift_1

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

The domain of a 2-morphism.

Equations

• (Mathlib.Tactic.BicategoryLike.WhiskerLeft.of η).srcM = η.srcM
• (Mathlib.Tactic.BicategoryLike.WhiskerLeft.whisker e f η).srcM = do let __do_lift ← η.srcM Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M (Mathlib.Tactic.BicategoryLike.Mor₁.of f) __do_lift

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

The codomain of a 2-morphism.

Equations

• (Mathlib.Tactic.BicategoryLike.WhiskerLeft.of η).tgtM = η.tgtM
• (Mathlib.Tactic.BicategoryLike.WhiskerLeft.whisker e f η).tgtM = do let __do_lift ← η.tgtM Mathlib.Tactic.BicategoryLike.MonadMor₁.comp₁M (Mathlib.Tactic.BicategoryLike.Mor₁.of f) __do_lift

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

The domain of a 2-morphism.

Equations

• (Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α).srcM = Mathlib.Tactic.BicategoryLike.Mor₂Iso.srcM α
• (Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs).srcM = Mathlib.Tactic.BicategoryLike.Mor₂Iso.srcM α

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

The codomain of a 2-morphism.

Equations

• (Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α).tgtM = Mathlib.Tactic.BicategoryLike.Mor₂Iso.tgtM α
• (Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs).tgtM = ηs.tgtM

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

The identity 2-morphism as a term of normalExpr.

Equations

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

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

The associator as a term of normalExpr.

Equations

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

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

The inverse of the associator as a term of normalExpr.

Equations

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

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

The left unitor as a term of normalExpr.

Equations

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

def Mathlib.Tactic.BicategoryLike.NormalExpr.leftUnitorInvM {m : Type → Type} [Monad m] [MonadMor₂Iso m] [MonadNormalExpr m] (f : Mor₁) : m 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.

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

The right unitor as a term of normalExpr.

Equations

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

def Mathlib.Tactic.BicategoryLike.NormalExpr.rightUnitorInvM {m : Type → Type} [Monad m] [MonadMor₂Iso m] [MonadNormalExpr m] (f : Mor₁) : m 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.

def Mathlib.Tactic.BicategoryLike.NormalExpr.ofM {m : Type → Type} [Monad m] [MonadMor₂Iso m] [MonadNormalExpr m] [MonadMor₁ m] (η : WhiskerLeft) : m NormalExpr

Construct a NormalExpr expression from a WhiskerLeft expression.

Equations

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

def Mathlib.Tactic.BicategoryLike.NormalExpr.ofAtomM {m : Type → Type} [Monad m] [MonadMor₂Iso m] [MonadNormalExpr m] [MonadMor₁ m] (η : Atom) : m 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.

def Mathlib.Tactic.BicategoryLike.NormalExpr.toList : NormalExpr → List WhiskerLeft

Convert a NormalExpr expression into a list of WhiskerLeft expressions.

Equations

• (Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α).toList = []
• (Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs).toList = η :: ηs.toList

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

The result of evaluating an expression into normal form.

• expr : NormalExpr

  The normalized expression of the 2-morphism.

• proof : Lean.Expr

  The proof that the normalized expression is equal to the original expression.

instance Mathlib.Tactic.BicategoryLike.Eval.instInhabitedResult : Inhabited Result

Equations

• Mathlib.Tactic.BicategoryLike.Eval.instInhabitedResult = { default := { expr := default, proof := default } }

class Mathlib.Tactic.BicategoryLike.MkEvalComp (m : Type → Type) : Type

Evaluate the expression α ≫ β.

• mkEvalCompNilNil (α β : Structural) : m Lean.Expr

  Evaluate α ≫ β

• mkEvalCompNilCons (α β : Structural) (η : WhiskerLeft) (ηs : NormalExpr) : m Lean.Expr

  Evaluate α ≫ (β ≫ η ≫ ηs)

• mkEvalCompCons (α : Structural) (η : WhiskerLeft) (ηs θ ι : NormalExpr) (e_η : Lean.Expr) : m Lean.Expr

  Evaluate (α ≫ η ≫ ηs) ≫ θ

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

Evaluatte the expression f ◁ η.

• mkEvalWhiskerLeftNil (f : Mor₁) (α : Structural) : m Lean.Expr

  Evaluatte f ◁ α

• mkEvalWhiskerLeftOfCons (f : Atom₁) (α : Structural) (η : WhiskerLeft) (ηs θ : NormalExpr) (e_θ : Lean.Expr) : m Lean.Expr

  Evaluate f ◁ (α ≫ η ≫ ηs).

• mkEvalWhiskerLeftComp (f g : Mor₁) (η η₁ η₂ η₃ η₄ : NormalExpr) (e_η₁ e_η₂ e_η₃ e_η₄ : Lean.Expr) : m Lean.Expr

  Evaluate (f ≫ g) ◁ η

• mkEvalWhiskerLeftId (η η₁ η₂ : NormalExpr) (e_η₁ e_η₂ : Lean.Expr) : m Lean.Expr

  Evaluate 𝟙 _ ◁ η

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

Evaluate the expression η ▷ f.

• mkEvalWhiskerRightAuxOf (η : WhiskerRight) (f : Atom₁) : m Lean.Expr

  Evaluate η ▷ f

• mkEvalWhiskerRightAuxCons (f : Atom₁) (η : WhiskerRight) (ηs : HorizontalComp) (ηs' η₁ η₂ η₃ : NormalExpr) (e_ηs' e_η₁ e_η₂ e_η₃ : Lean.Expr) : m Lean.Expr

  Evaluate (η ◫ ηs) ▷ f

• mkEvalWhiskerRightNil (α : Structural) (f : Mor₁) : m Lean.Expr

  Evaluate α ▷ f

• mkEvalWhiskerRightConsOfOf (f : Atom₁) (α : Structural) (η : HorizontalComp) (ηs ηs₁ η₁ η₂ η₃ : NormalExpr) (e_ηs₁ e_η₁ e_η₂ e_η₃ : Lean.Expr) : m Lean.Expr

  Evaluate (α ≫ η ≫ ηs) ▷ j

• mkEvalWhiskerRightConsWhisker (f : Atom₁) (g : Mor₁) (α : Structural) (η : WhiskerLeft) (ηs η₁ η₂ ηs₁ ηs₂ η₃ η₄ η₅ : NormalExpr) (e_η₁ e_η₂ e_ηs₁ e_ηs₂ e_η₃ e_η₄ e_η₅ : Lean.Expr) : m Lean.Expr

  Evaluate (α ≫ (f ◁ η) ≫ ηs) ▷ g

• mkEvalWhiskerRightComp (g h : Mor₁) (η η₁ η₂ η₃ η₄ : NormalExpr) (e_η₁ e_η₂ e_η₃ e_η₄ : Lean.Expr) : m Lean.Expr

  Evaluate η ▷ (g ⊗ h)

• mkEvalWhiskerRightId (η η₁ η₂ : NormalExpr) (e_η₁ e_η₂ : Lean.Expr) : m Lean.Expr

  Evaluate η ▷ 𝟙 _

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

Evaluate the expression η ◫ θ.

• mkEvalHorizontalCompAuxOf (η : WhiskerRight) (θ : HorizontalComp) : m Lean.Expr

  Evaluate η ◫ θ

• mkEvalHorizontalCompAuxCons (η : WhiskerRight) (ηs θ : HorizontalComp) (ηθ η₁ ηθ₁ ηθ₂ : NormalExpr) (e_ηθ e_η₁ e_ηθ₁ e_ηθ₂ : Lean.Expr) : m Lean.Expr

  Evaluate (η ◫ ηs) ◫ θ

• mkEvalHorizontalCompAux'Whisker (f : Atom₁) (η θ : WhiskerLeft) (ηθ ηθ₁ ηθ₂ ηθ₃ : NormalExpr) (e_ηθ e_ηθ₁ e_ηθ₂ e_ηθ₃ : Lean.Expr) : m Lean.Expr

  Evaluate (f ◁ η) ◫ θ

• mkEvalHorizontalCompAux'OfWhisker (f : Atom₁) (η : HorizontalComp) (θ : WhiskerLeft) (η₁ ηθ ηθ₁ ηθ₂ : NormalExpr) (e_ηθ e_η₁ e_ηθ₁ e_ηθ₂ : Lean.Expr) : m Lean.Expr

  Evaluate η ◫ (f ◁ θ)

• mkEvalHorizontalCompNilNil (α β : Structural) : m Lean.Expr

  Evaluate α ◫ β

• mkEvalHorizontalCompNilCons (α β : Structural) (η : WhiskerLeft) (ηs η₁ ηs₁ η₂ η₃ : NormalExpr) (e_η₁ e_ηs₁ e_η₂ e_η₃ : Lean.Expr) : m Lean.Expr

  Evaluate α ◫ (β ≫ η ≫ ηs)

• mkEvalHorizontalCompConsNil (α β : Structural) (η : WhiskerLeft) (ηs η₁ ηs₁ η₂ η₃ : NormalExpr) (e_η₁ e_ηs₁ e_η₂ e_η₃ : Lean.Expr) : m Lean.Expr

  Evaluate (α ≫ η ≫ ηs) ◫ β

• mkEvalHorizontalCompConsCons (α β : Structural) (η θ : WhiskerLeft) (ηs θs ηθ ηθs ηθ₁ ηθ₂ : NormalExpr) (e_ηθ e_ηθs e_ηθ₁ e_ηθ₂ : Lean.Expr) : m Lean.Expr

  Evaluate (α ≫ η ≫ ηs) ◫ (β ≫ θ ≫ θs)

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

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

• mkEvalCompNilNil (α β : Structural) : m Lean.Expr
• mkEvalCompNilCons (α β : Structural) (η : WhiskerLeft) (ηs : NormalExpr) : m Lean.Expr
• mkEvalCompCons (α : Structural) (η : WhiskerLeft) (ηs θ ι : NormalExpr) (e_η : Lean.Expr) : m Lean.Expr
• mkEvalWhiskerLeftNil (f : Mor₁) (α : Structural) : m Lean.Expr
• mkEvalWhiskerLeftOfCons (f : Atom₁) (α : Structural) (η : WhiskerLeft) (ηs θ : NormalExpr) (e_θ : Lean.Expr) : m Lean.Expr
• mkEvalWhiskerLeftComp (f g : Mor₁) (η η₁ η₂ η₃ η₄ : NormalExpr) (e_η₁ e_η₂ e_η₃ e_η₄ : Lean.Expr) : m Lean.Expr
• mkEvalWhiskerLeftId (η η₁ η₂ : NormalExpr) (e_η₁ e_η₂ : Lean.Expr) : m Lean.Expr
• mkEvalWhiskerRightAuxOf (η : WhiskerRight) (f : Atom₁) : m Lean.Expr
• mkEvalWhiskerRightAuxCons (f : Atom₁) (η : WhiskerRight) (ηs : HorizontalComp) (ηs' η₁ η₂ η₃ : NormalExpr) (e_ηs' e_η₁ e_η₂ e_η₃ : Lean.Expr) : m Lean.Expr
• mkEvalWhiskerRightNil (α : Structural) (f : Mor₁) : m Lean.Expr
• mkEvalWhiskerRightConsOfOf (f : Atom₁) (α : Structural) (η : HorizontalComp) (ηs ηs₁ η₁ η₂ η₃ : NormalExpr) (e_ηs₁ e_η₁ e_η₂ e_η₃ : Lean.Expr) : m Lean.Expr
• mkEvalWhiskerRightConsWhisker (f : Atom₁) (g : Mor₁) (α : Structural) (η : WhiskerLeft) (ηs η₁ η₂ ηs₁ ηs₂ η₃ η₄ η₅ : NormalExpr) (e_η₁ e_η₂ e_ηs₁ e_ηs₂ e_η₃ e_η₄ e_η₅ : Lean.Expr) : m Lean.Expr
• mkEvalWhiskerRightComp (g h : Mor₁) (η η₁ η₂ η₃ η₄ : NormalExpr) (e_η₁ e_η₂ e_η₃ e_η₄ : Lean.Expr) : m Lean.Expr
• mkEvalWhiskerRightId (η η₁ η₂ : NormalExpr) (e_η₁ e_η₂ : Lean.Expr) : m Lean.Expr
• mkEvalHorizontalCompAuxOf (η : WhiskerRight) (θ : HorizontalComp) : m Lean.Expr
• mkEvalHorizontalCompAuxCons (η : WhiskerRight) (ηs θ : HorizontalComp) (ηθ η₁ ηθ₁ ηθ₂ : NormalExpr) (e_ηθ e_η₁ e_ηθ₁ e_ηθ₂ : Lean.Expr) : m Lean.Expr
• mkEvalHorizontalCompAux'Whisker (f : Atom₁) (η θ : WhiskerLeft) (ηθ ηθ₁ ηθ₂ ηθ₃ : NormalExpr) (e_ηθ e_ηθ₁ e_ηθ₂ e_ηθ₃ : Lean.Expr) : m Lean.Expr
• mkEvalHorizontalCompAux'OfWhisker (f : Atom₁) (η : HorizontalComp) (θ : WhiskerLeft) (η₁ ηθ ηθ₁ ηθ₂ : NormalExpr) (e_ηθ e_η₁ e_ηθ₁ e_ηθ₂ : Lean.Expr) : m Lean.Expr
• mkEvalHorizontalCompNilNil (α β : Structural) : m Lean.Expr
• mkEvalHorizontalCompNilCons (α β : Structural) (η : WhiskerLeft) (ηs η₁ ηs₁ η₂ η₃ : NormalExpr) (e_η₁ e_ηs₁ e_η₂ e_η₃ : Lean.Expr) : m Lean.Expr
• mkEvalHorizontalCompConsNil (α β : Structural) (η : WhiskerLeft) (ηs η₁ ηs₁ η₂ η₃ : NormalExpr) (e_η₁ e_ηs₁ e_η₂ e_η₃ : Lean.Expr) : m Lean.Expr
• mkEvalHorizontalCompConsCons (α β : Structural) (η θ : WhiskerLeft) (ηs θs ηθ ηθs ηθ₁ ηθ₂ : NormalExpr) (e_ηθ e_ηθs e_ηθ₁ e_ηθ₂ : Lean.Expr) : m Lean.Expr
• mkEvalComp (η θ : Mor₂) (η' θ' ηθ : NormalExpr) (e_η e_θ e_ηθ : Lean.Expr) : m Lean.Expr

  Evaluate the expression η ≫ θ into a normalized form.

• mkEvalWhiskerLeft (f : Mor₁) (η : Mor₂) (η' θ : NormalExpr) (e_η e_θ : Lean.Expr) : m Lean.Expr

  Evaluate the expression f ◁ η into a normalized form.

• mkEvalWhiskerRight (η : Mor₂) (h : Mor₁) (η' θ : NormalExpr) (e_η e_θ : Lean.Expr) : m Lean.Expr

  Evaluate the expression η ▷ f into a normalized form.

• mkEvalHorizontalComp (η θ : Mor₂) (η' θ' ι : NormalExpr) (e_η e_θ e_ι : Lean.Expr) : m Lean.Expr

  Evaluate the expression η ◫ θ into a normalized form.

• mkEvalOf (η : Atom) : m Lean.Expr

  Evaluate the atomic 2-morphism η into a normalized form.

• mkEvalMonoidalComp (η θ : Mor₂) (α : Structural) (η' θ' αθ ηαθ : NormalExpr) (e_η e_θ e_αθ e_ηαθ : Lean.Expr) : m Lean.Expr

  Evaluate the expression η ⊗≫ θ := η ≫ α ≫ θ into a normalized form.

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

Evaluate the expression α ≫ η into a normalized form.

Equations

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

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

Evaluate the expression η ≫ θ into a normalized form.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.BicategoryLike.evalComp (Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α) x✝ = Mathlib.Tactic.BicategoryLike.evalCompNil α x✝

@[irreducible]

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

Evaluate the expression f ◁ η into a normalized form.

Equations

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

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

Evaluate the expression η ▷ f into a normalized form.

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

Evaluate the expression η ▷ f into a normalized form.

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

Evaluate the expression η ⊗ θ into a normalized form.

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

Evaluate the expression η ⊗ θ into a normalized form.

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

Evaluate the expression η ⊗ θ into a normalized form.

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

Trace the proof of the normalization.

Equations

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

def Mathlib.Tactic.BicategoryLike.eval {ρ : Type} [MonadMor₁ (CoherenceM ρ)] [MonadMor₂Iso (CoherenceM ρ)] [MonadNormalExpr (CoherenceM ρ)] [MkEval (CoherenceM ρ)] [MonadMor₂ (CoherenceM ρ)] (nm : Lean.Name) (e : Mor₂) : CoherenceM ρ Eval.Result

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