mathlib documentation


Unbundled lax monoidal functors

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.


Construct a bundled lax_monoidal_functor from the object level function and functorial and lax_monoidal typeclasses.