Theorems · Inductive type · category theory

CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore

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

An InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D bundles the core data needed to construct a full LawfulDayConvolutionMonoidalCategoryStructCore. We are making this a class so that it can act as a "proxy" for inferring DayConvolution instances (which is all the more important that we are modifying the instances given in the constructor to get better ones defeq-wise). As this object is purely about the internals of definitions of Day convolutions monoidal structures, it is advised to not register this class globally.

Defined in

Mathlib.CategoryTheory.Monoidal.DayConvolution

Cited by

5 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalCategoryCategoryTheory.Category