Auxilliary definition of monoidal_coherence, being careful with namespaces to avoid shadowing.

Coherence tactic for monoidal categories.

pure_coherence uses the coherence theorem for monoidal categories to prove the goal. It can prove any equality made up only of associators, unitors, and identities.

example {C : Type} [category C] [monoidal_category C] :
  (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom :=
by pure_coherence

Users will typicall just use the coherence tactic, which can also cope with identities of the form a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c' where a = a', b = b', and c = c' can be proved using pure_coherence

Internal tactic used in coherence.

Rewrites an equation f = g as f₀ ≫ f₁ = g₀ ≫ g₁, where f₀ and g₀ are maximal prefixes of f and g (possibly after reassociating) which are "liftable" (i.e. expressible as compositions of unitors and associators).

The main part of coherence tactic.

Use the coherence theorem for monoidal categories to solve equations in a monoidal equation, where the two sides only differ by replacing strings of monoidal structural morphisms (that is, associators, unitors, and identities) with different strings of structural morphisms with the same source and target.

That is, coherence can handle goals of the form a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c' where a = a', b = b', and c = c' can be proved using pure_coherence.

(If you have very large equations on which coherence is unexpectedly failing, you may need to increase the typeclass search depth, using e.g. set_option class.instance_max_depth 500.)

pure_coherence uses the coherence theorem for monoidal categories to prove the goal. It can prove any equality made up only of associators, unitors, and identities.

example {C : Type} [category C] [monoidal_category C] :
  (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom :=
by pure_coherence

Users will typicall just use the coherence tactic, which can also cope with identities of the form a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c' where a = a', b = b', and c = c' can be proved using pure_coherence

Use the coherence theorem for monoidal categories to solve equations in a monoidal equation, where the two sides only differ by replacing strings of monoidal structural morphisms (that is, associators, unitors, and identities) with different strings of structural morphisms with the same source and target.

That is, coherence can handle goals of the form a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c' where a = a', b = b', and c = c' can be proved using pure_coherence.

(If you have very large equations on which coherence is unexpectedly failing, you may need to increase the typeclass search depth, using e.g. set_option class.instance_max_depth 500.)