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.

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

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