# 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'`.

source
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`.

Instances For

source
instance Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerRight :
Inhabited WhiskerRight
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerRight = { default := Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerRight.default }

source
def Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerRight.default :
WhiskerRight
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerRight.default = Mathlib.Tactic.BicategoryLike.WhiskerRight.of default

Instances For

source
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

Instances For

source
inductive Mathlib.Tactic.BicategoryLike.HorizontalComp :
Type

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

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

Instances For

source
instance Mathlib.Tactic.BicategoryLike.instInhabitedHorizontalComp :
Inhabited HorizontalComp
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedHorizontalComp = { default := Mathlib.Tactic.BicategoryLike.instInhabitedHorizontalComp.default }

source
def Mathlib.Tactic.BicategoryLike.instInhabitedHorizontalComp.default :
HorizontalComp
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedHorizontalComp.default = Mathlib.Tactic.BicategoryLike.HorizontalComp.of default

Instances For

source
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

Instances For

source
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 ◁ η`.

Instances For

source
def Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerLeft.default :
WhiskerLeft
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerLeft.default = Mathlib.Tactic.BicategoryLike.WhiskerLeft.of default

Instances For

source
instance Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerLeft :
Inhabited WhiskerLeft
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerLeft = { default := Mathlib.Tactic.BicategoryLike.instInhabitedWhiskerLeft.default }

source
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

Instances For

source
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

Instances For

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

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

Instances For

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

Instances For

source
instance Mathlib.Tactic.BicategoryLike.instInhabitedNormalExpr :
Inhabited NormalExpr
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedNormalExpr = { default := Mathlib.Tactic.BicategoryLike.instInhabitedNormalExpr.default }

source
def Mathlib.Tactic.BicategoryLike.instInhabitedNormalExpr.default :
NormalExpr
Equations

- Mathlib.Tactic.BicategoryLike.instInhabitedNormalExpr.default = Mathlib.Tactic.BicategoryLike.NormalExpr.nil default default

Instances For

source
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

Instances For

source
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`.

Instances

source
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`.

Instances

source
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 ▷ η`.

Instances

source
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`.

Instances

source
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)

Instances For

source
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)

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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 α

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

source
def Mathlib.Tactic.BicategoryLike.Eval.instInhabitedResult.default :
Result
Equations

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

Instances For

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

- Mathlib.Tactic.BicategoryLike.Eval.instInhabitedResult = { default := Mathlib.Tactic.BicategoryLike.Eval.instInhabitedResult.default }

source
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) ≫ θ`

Instances

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

Evaluate the expression `f ◁ η`.

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

  Evaluate `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 `𝟙 _ ◁ η`

Instances

source
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 `η ▷ 𝟙 _`

Instances

source
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)`

Instances

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

Instances

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

Instances For

source
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✝

Instances For

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

Instances For

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

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

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

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

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

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

Instances For

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

Instances For