# Documentation

Mathlib.CategoryTheory.Monoidal.Functorial

# 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' : LaxMonoidalFunctor C D, and assert F'.toFunctor ≅ F.
2. Introduce unbundled functors and unbundled lax monoidal functors, and construct LaxMonoidal F.obj, then construct F' := LaxMonoidalFunctor.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.

class CategoryTheory.LaxMonoidal {C : Type u₁} [] {D : Type u₂} [] (F : CD) :
Type (max u₁ v₂)

An unbundled description of lax monoidal functors.

Instances
@[simp]
theorem CategoryTheory.LaxMonoidalFunctor.of_ε {C : Type u₁} [] {D : Type u₂} [] (F : CD) [I₁ : ] [I₂ : ] :
= CategoryTheory.LaxMonoidal.ε
@[simp]
theorem CategoryTheory.LaxMonoidalFunctor.of_toFunctor_map {C : Type u₁} [] {D : Type u₂} [] (F : CD) [I₁ : ] [I₂ : ] :
∀ {X Y : C} (f : X Y), ().toFunctor.map f =
@[simp]
theorem CategoryTheory.LaxMonoidalFunctor.of_μ {C : Type u₁} [] {D : Type u₂} [] (F : CD) [I₁ : ] [I₂ : ] (X : C) (Y : C) :
@[simp]
theorem CategoryTheory.LaxMonoidalFunctor.of_toFunctor_obj {C : Type u₁} [] {D : Type u₂} [] (F : CD) [I₁ : ] [I₂ : ] :
∀ (a : C), ().toFunctor.obj a = F a
def CategoryTheory.LaxMonoidalFunctor.of {C : Type u₁} [] {D : Type u₂} [] (F : CD) [I₁ : ] [I₂ : ] :

Construct a bundled LaxMonoidalFunctor from the object level function and Functorial and LaxMonoidal typeclasses.

Instances For
instance CategoryTheory.laxMonoidalId {C : Type u₁} [] :