# 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.LaxMonoidal.μ_natural_left {C : Type u₁} [] {D : Type u₂} [] {F : CD} [self : ] {X : C} {Y : C} (f : X Y) (X' : C) :
@[simp]
theorem CategoryTheory.LaxMonoidal.μ_natural_right {C : Type u₁} [] {D : Type u₂} [] {F : CD} [self : ] {X : C} {Y : C} (X' : C) (f : X Y) :
@[simp]
theorem CategoryTheory.LaxMonoidal.associativity {C : Type u₁} [] {D : Type u₂} [] {F : CD} [self : ] (X : C) (Y : C) (Z : C) :

associativity of the tensorator

theorem CategoryTheory.LaxMonoidal.left_unitality {C : Type u₁} [] {D : Type u₂} [] {F : CD} [self : ] (X : C) :

left unitality

theorem CategoryTheory.LaxMonoidal.right_unitality {C : Type u₁} [] {D : Type u₂} [] {F : CD} [self : ] (X : C) :

right unitality

@[reducible, inline]
abbrev CategoryTheory.LaxMonoidal.ofTensorHom {C : Type u₁} [] {D : Type u₂} [] (F : CD) (ε : 𝟙_ D F (𝟙_ C)) (μ : (X Y : C) → ) (μ_natural : autoParam (∀ {X Y X' Y' : C} (f : X Y) (g : X' Y'), = ) _auto✝) (associativity : autoParam (∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp () () = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F X) (F Y) (F Z)).hom ()) _auto✝) (left_unitality : autoParam (∀ (X : C), .hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (μ (𝟙_ C) X) )) _auto✝) (right_unitality : autoParam (∀ (X : C), .hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (μ X (𝟙_ C)) )) _auto✝) :

An unbundled description of lax monoidal functors.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.LaxMonoidalFunctor.of_toFunctor_obj {C : Type u₁} [] {D : Type u₂} [] (F : CD) [I₁ : ] [I₂ : ] :
∀ (a : C), a = F a
@[simp]
theorem CategoryTheory.LaxMonoidalFunctor.of_ε {C : Type u₁} [] {D : Type u₂} [] (F : CD) [I₁ : ] [I₂ : ] :
= CategoryTheory.LaxMonoidal.ε
@[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_map {C : Type u₁} [] {D : Type u₂} [] (F : CD) [I₁ : ] [I₂ : ] :
∀ {X Y : C} (f : X Y),
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance CategoryTheory.instLaxMonoidalObj {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Equations
• = { ε := F, μ := F, μ_natural_left := , μ_natural_right := , associativity := , left_unitality := , right_unitality := }
instance CategoryTheory.laxMonoidalId {C : Type u₁} [] :
Equations
• One or more equations did not get rendered due to their size.