mathlib

d047eb46 - feat(category_theory/monoidal): upgrades for monoidal equivalences (#13158)

feat(category_theory/monoidal): upgrades for monoidal equivalences (#13158) (Recall that a "monoidal equivalence" is a functor which is separately monoidal, and an equivalence. This PR completes the work required to see this is the same as having a monoidal inverse, up to monoidal units and counits.) * Shows that the unit and counit of a monoidal equivalence have a natural monoidal structure. * Previously, when transporting a monoidal structure across a (non-monoidal) equivalence, we constructed directly the monoidal strength on the inverse functor. In the meantime, @b-mehta has provided a general construction for the monoidal strength on the inverse of any monoidal equivalence, so now we use that. The proofs of `monoidal_unit` and `monoidal_counit` in `category_theory/monoidal/natural_transformation.lean` are quite ugly. If anyone would like to golf these that would be lovely! :-) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>