Theorems · Definition · category theory

CategoryTheory.Center.Hom.recOn

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y : CategoryTheory.Center C} →
        {motive : X.Hom Y → Sort u} →
          (t : X.Hom Y) →
            ((f : X.fst ⟶ Y.fst) →
                (comm :
                    ∀ (U : C),
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f U)
                          (Y.snd.β U).hom =
                        CategoryTheory.CategoryStruct.comp (X.snd.β U).hom
                          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U f)) →
                  motive { f := f, comm := comm }) →
              motive t

Defined in

Mathlib.CategoryTheory.Monoidal.Center

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategory