Monoidal natural transformations #
Natural transformations between (lax) monoidal functors must satisfy
an additional compatibility relation with the tensorators:
F.μ X Y ≫ app (X ⊗ Y) = (app X ⊗ app Y) ≫ G.μ X Y
.
(Lax) monoidal functors between a fixed pair of monoidal categories themselves form a category.
- app : (X : C) → F.obj X ⟶ G.obj X
- naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (s.app Y) = CategoryTheory.CategoryStruct.comp (s.app X) (G.map f)
- unit : CategoryTheory.CategoryStruct.comp F.ε (s.app (CategoryTheory.MonoidalCategory.tensorUnit C)) = G.ε
The unit condition for a monoidal natural transformation.
- tensor : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ F X Y) (s.app (CategoryTheory.MonoidalCategory.tensorObj X Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (s.app X) (s.app Y)) (CategoryTheory.LaxMonoidalFunctor.μ G X Y)
The tensor condition for a monoidal natural transformation.
A monoidal natural transformation is a natural transformation between (lax) monoidal functors
additionally satisfying:
F.μ X Y ≫ app (X ⊗ Y) = (app X ⊗ app Y) ≫ G.μ X Y
Instances For
The identity monoidal natural transformation.
Instances For
Vertical composition of monoidal natural transformations.
Instances For
Horizontal composition of monoidal natural transformations.
Instances For
The cartesian product of two monoidal natural transformations is monoidal.
Instances For
Construct a monoidal natural isomorphism from object level isomorphisms, and the monoidal naturality in the forward direction.
Instances For
The unit of a monoidal equivalence can be upgraded to a monoidal natural transformation.
Instances For
The counit of a monoidal equivalence can be upgraded to a monoidal natural transformation.