mathlib3 documentation


Unbundled lax monoidal functors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Design considerations #

The essential problem I've encountered that requires unbundled functors is having an existing (non-monoidal) functor F : C ⥤ D between monoidal categories, and wanting to assert that it has an extension to a lax monoidal functor.

The two options seem to be

  1. Construct a separate F' : lax_monoidal_functor C D, and assert F'.to_functor ≅ F.
  2. Introduce unbundled functors and unbundled lax monoidal functors, and construct lax_monoidal F.obj, then construct F' := lax_monoidal_functor.of F.obj.

Both have costs, but as for option 2. the cost is in library design, while in option 1. the cost is users having to carry around additional isomorphisms forever, I wanted to introduce unbundled functors.

TODO: later, we may want to do this for strong monoidal functors as well, but the immediate application, for enriched categories, only requires this notion.


An unbundled description of lax monoidal functors.

Instances of this typeclass
Instances of other typeclasses for category_theory.lax_monoidal
  • category_theory.lax_monoidal.has_sizeof_inst