mathlib

953a5dc0 - feat(category_theory/monoidal): monoid objects are just lax monoidal functors from punit (#4121)