Commit 2021-02-26 23:38 d38b5a50
View on Github →feat(category_theory/monoidal): construct the monoidal inverse to a functor (#6442) I worked out what was mentioned here: https://github.com/leanprover-community/mathlib/blob/20b49fbd453fc42c91c36ee30ecb512d70f48172/src/category_theory/monoidal/transport.lean#L283-L287 except for uniqueness, not sure how important that is