Mathlib Map

Structures · Category theory

CategoryTheory.NatTrans.IsMonoidal

A natural transformation between (lax) monoidal functors is monoidal if it satisfies ε F ≫ τ.app (𝟙_ C) = ε G and μ F X Y ≫ app (X ⊗ Y) = (app X ⊗ₘ app Y) ≫ μ G X Y.

Defined in
Mathlib.CategoryTheory.Monoidal.NaturalTransformation
Shape
One type argument · adds unit, tensor
Open in Mathlib docs

Extends0

Extends nothing: this is a root of the hierarchy.

Extended by0

Nothing extends this class yet.

Concrete types that are instances3

  • CategoryTheory.Functor
  • CategoryTheory.Discrete
  • CategoryTheory.Monoidal.Transported

How is a type an instance?

Loading the hierarchy index…

Assumed by44

Ancestors0

No ancestors.