Theorems · Inductive type · category theory

CategoryTheory.Functor.CoreMonoidal

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [CategoryTheory.MonoidalCategory D] → CategoryTheory.Functor C D → Type (max u₁ v₂)

Structure which is a helper in order to show that a functor is monoidal. It consists of isomorphisms εIso and μIso such that the morphisms .hom induced by these isomorphisms satisfy the axioms of lax monoidal functors.

Defined in

Mathlib.CategoryTheory.Monoidal.Functor

Cited by

21 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategory