Commit 2022-04-07 07:05 d047eb46

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! :-)