1. Overview
The tactic
monoidal
solves equalities of morphisms in monoidal categories,
and
the tactic
bicategory
solves equalities of 2-morphisms in bicategories.
These tactics solve goals when the two sides differ only by associators and unitors. The
mathematical background is the coherence theorem: internally, the general coherence equalities
needed to solve such goals are generated from the pentagon and triangle identities.
In practice, these tactics are often used to close individual steps inside a calc proof. Write the sequence of
mathematically meaningful rewrites as the lines of the calc. To use rw, one often has to
place parentheses appropriately so that the rewriting lemma at hand applies, such as
whisker_exchange, a naturality lemma, or an
application-specific identity. This creates
intermediate goals where the two sides
differ only by associators and unitors. At those points, apply
monoidal
or
bicategory
to close the step.
A typical example is the construction showing that an equivalence datum, not yet known to satisfy the triangle identities, can be upgraded to an adjoint equivalence by replacing the counit. The proof below is the left triangle identity for the upgraded counit:
abbrev adjointifyCounit_hom (η : 𝟙 a ≅ f ≫ g) (ε : g ≫ f ≅ 𝟙 b) :
g ≫ f ⟶ 𝟙 b :=
g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.homtheorem adjointifyCounit_left_triangle (η : 𝟙 a ≅ f ≫ g) (ε : g ≫ f ≅ 𝟙 b) :
leftZigzag η.hom (adjointifyCounit_hom η ε) = (λ_ f).hom ≫ (ρ_ f).inv := B:Type uinst✝:Bicategory Ba:Bb:Bf:a ⟶ bg:b ⟶ aη:𝟙 a ≅ f ≫ gε:g ≫ f ≅ 𝟙 b⊢ leftZigzag η.hom (adjointifyCounit_hom η ε) = (λ_ f).hom ≫ (ρ_ f).inv
with_panel_widgets [Mathlib.Tactic.Widget.StringDiagram]
calc
_ = 𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫
f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom := B:Type uinst✝:Bicategory Ba:Bb:Bf:a ⟶ bg:b ⟶ aη:𝟙 a ≅ f ≫ gε:g ≫ f ≅ 𝟙 b⊢ leftZigzag η.hom (adjointifyCounit_hom η ε) =
𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom
All goals completed! 🐙
_ = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫
(η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom := B:Type uinst✝:Bicategory Ba:Bb:Bf:a ⟶ bg:b ⟶ aη:𝟙 a ≅ f ≫ gε:g ≫ f ≅ 𝟙 b⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom
B:Type uinst✝:Bicategory Ba:Bb:Bf:a ⟶ bg:b ⟶ aη:𝟙 a ≅ f ≫ gε:g ≫ f ≅ 𝟙 b⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ (𝟙 a ◁ f ◁ ε.inv ≫ η.hom ▷ (f ≫ g ≫ f)) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom
All goals completed! 🐙
_ = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom := B:Type uinst✝:Bicategory Ba:Bb:Bf:a ⟶ bg:b ⟶ aη:𝟙 a ≅ f ≫ gε:g ≫ f ≅ 𝟙 b⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom =
𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom
B:Type uinst✝:Bicategory Ba:Bb:Bf:a ⟶ bg:b ⟶ aη:𝟙 a ≅ f ≫ gε:g ≫ f ≅ 𝟙 b⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (𝟙 a ◁ η.inv ≫ η.hom ▷ 𝟙 a) ▷ f ⊗≫ f ◁ ε.hom =
𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom
All goals completed! 🐙
_ = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom) := B:Type uinst✝:Bicategory Ba:Bb:Bf:a ⟶ bg:b ⟶ aη:𝟙 a ≅ f ≫ gε:g ≫ f ≅ 𝟙 b⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom)
B:Type uinst✝:Bicategory Ba:Bb:Bf:a ⟶ bg:b ⟶ aη:𝟙 a ≅ f ≫ gε:g ≫ f ≅ 𝟙 b⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ 𝟙 (f ≫ g) ▷ f ⊗≫ f ◁ ε.hom = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom)
All goals completed! 🐙
_ = _ := B:Type uinst✝:Bicategory Ba:Bb:Bf:a ⟶ bg:b ⟶ aη:𝟙 a ≅ f ≫ gε:g ≫ f ≅ 𝟙 b⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv
B:Type uinst✝:Bicategory Ba:Bb:Bf:a ⟶ bg:b ⟶ aη:𝟙 a ≅ f ≫ gε:g ≫ f ≅ 𝟙 b⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ 𝟙 (𝟙 b) = (λ_ f).hom ≫ (ρ_ f).inv
All goals completed! 🐙
The visible rewrites are the two uses of
whisker_exchange
and the cancellations of η.inv ≫ η.hom and ε.inv ≫ ε.hom. After each such step,
bicategory
solves the remaining equality, where the only difference is in associators and unitors.
The proof above can be visualized with the string diagram widget
Mathlib.Tactic.Widget.StringDiagram
as a sequence of string diagrams. Verso does not display the widget directly yet, so instead the
diagrams are shown below without mouseover Lean information:
Step 1.
Step 2.
Step 3.
Step 4.
Step 5.