Theorems · Definition · category theory

CategoryTheory.Center.Hom.mk.noConfusion

{C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {X Y : CategoryTheory.Center C} →
        {P : Sort u} →
          {f : X.fst ⟶ Y.fst} →
            {comm :
                autoParam
                  (∀ (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))
                  CategoryTheory.Center.Hom.comm._autoParam} →
              {f' : X.fst ⟶ Y.fst} →
                {comm' :
                    autoParam
                      (∀ (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'))
                      CategoryTheory.Center.Hom.comm._autoParam} →
                  { f := f, comm := comm } = { f := f', comm := comm' } → (f ≍ f' → P) → P

Defined in

Mathlib.CategoryTheory.Monoidal.Center

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms