Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-18 09:43 953a5dc0

View on Github →

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

Estimated changes

Modified src/category_theory/monoidal/internal.lean

added def Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal

added def Mon_.equiv_lax_monoidal_functor_punit.counit_iso

added def Mon_.equiv_lax_monoidal_functor_punit.lax_monoidal_to_Mon

added def Mon_.equiv_lax_monoidal_functor_punit.unit_iso

added def Mon_.equiv_lax_monoidal_functor_punit

Modified src/category_theory/monoidal/natural_transformation.lean

added theorem category_theory.monoidal_nat_iso.of_components.hom_app

added theorem category_theory.monoidal_nat_iso.of_components.inv_app

added def category_theory.monoidal_nat_iso.of_components

added theorem category_theory.monoidal_nat_trans.comp_to_nat_trans''

added theorem category_theory.monoidal_nat_trans.comp_to_nat_trans'

Modified src/category_theory/natural_isomorphism.lean