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/Widget/StringDiagram.lean, as well as monoidal and bicategory tactics.

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

η is of the form α₀ ≫ η₀ ≫ α₁ ≫ η₁ ≫ ... αₘ ≫ ηₘ ≫ αₘ₊₁ where each αᵢ is a structural 2-morphism (consisting of associators and unitors),
each ηᵢ is a non-structural 2-morphism of the form f₁ ◁ ... ◁ fₙ ◁ θ, and
θ is of the form ι₁ ◫ ... ◫ ιₗ, and
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 ProofWidgets. 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'.