# Commit 2022-04-07 07:05 d047eb46

View on Github →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! :-)