Theorems · Definition · category theory

CategoryTheory.HalfBraiding.mk.noConfusion

{C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {X : C} →
        {P : Sort u} →
          {β :
              (U : C) →
                CategoryTheory.MonoidalCategoryStruct.tensorObj X U ≅
                  CategoryTheory.MonoidalCategoryStruct.tensorObj U X} →
            {monoidal :
                autoParam
                  (∀ (U U' : C),
                    (β (CategoryTheory.MonoidalCategoryStruct.tensorObj U U')).hom =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X U U').inv
                        (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β U).hom U')
                          (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.associator U X U').hom
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U (β U').hom)
                              (CategoryTheory.MonoidalCategoryStruct.associator U U' X).inv))))
                  CategoryTheory.HalfBraiding.monoidal._autoParam} →
              {naturality :
                  autoParam
                    (∀ {U U' : C} (f : U ⟶ U'),
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
                          (β U').hom =
                        CategoryTheory.CategoryStruct.comp (β U).hom
                          (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X))
                    CategoryTheory.HalfBraiding.naturality._autoParam} →
                {β' :
                    (U : C) →
                      CategoryTheory.MonoidalCategoryStruct.tensorObj X U ≅
                        CategoryTheory.MonoidalCategoryStruct.tensorObj U X} →
                  {monoidal' :
                      autoParam
                        (∀ (U U' : C),
                          (β' (CategoryTheory.MonoidalCategoryStruct.tensorObj U U')).hom =
                            CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategoryStruct.associator X U U').inv
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β' U).hom U')
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.MonoidalCategoryStruct.associator U X U').hom
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U (β' U').hom)
                                    (CategoryTheory.MonoidalCategoryStruct.associator U U' X).inv))))
                        CategoryTheory.HalfBraiding.monoidal._autoParam} →
                    {naturality' :
                        autoParam
                          (∀ {U U' : C} (f : U ⟶ U'),
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
                                (β' U').hom =
                              CategoryTheory.CategoryStruct.comp (β' U).hom
                                (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X))
                          CategoryTheory.HalfBraiding.naturality._autoParam} →
                      { β := β, monoidal := monoidal, naturality := naturality } =
                          { β := β', monoidal := monoidal', naturality := naturality' } →
                        (β ≍ β' → P) → P

Defined in

Mathlib.CategoryTheory.Monoidal.Center

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms