Theorems · Definition · category theory

CategoryTheory.CopyDiscardCategory.mk.noConfusion

{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {P : Sort u_1} →
        {toSymmetricCategory : CategoryTheory.SymmetricCategory C} →
          {comonObj : (X : C) → CategoryTheory.ComonObj X} →
            {isCommComonObj : ∀ (X : C), CategoryTheory.IsCommComonObj X} →
              {copy_tensor :
                  autoParam
                    (∀ (X Y : C),
                      CategoryTheory.ComonObj.comul =
                        CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul
                            CategoryTheory.ComonObj.comul)
                          (CategoryTheory.MonoidalCategory.tensorμ X X Y Y))
                    CategoryTheory.CopyDiscardCategory.copy_tensor._autoParam} →
                {discard_tensor :
                    autoParam
                      (∀ (X Y : C),
                        CategoryTheory.ComonObj.counit =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.counit
                              CategoryTheory.ComonObj.counit)
                            (CategoryTheory.MonoidalCategoryStruct.leftUnitor
                                (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom)
                      CategoryTheory.CopyDiscardCategory.discard_tensor._autoParam} →
                  {copy_unit :
                      autoParam
                        (CategoryTheory.ComonObj.comul =
                          (CategoryTheory.MonoidalCategoryStruct.leftUnitor
                              (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv)
                        CategoryTheory.CopyDiscardCategory.copy_unit._autoParam} →
                    {discard_unit :
                        autoParam
                          (CategoryTheory.ComonObj.counit =
                            CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                          CategoryTheory.CopyDiscardCategory.discard_unit._autoParam} →
                      {toSymmetricCategory' : CategoryTheory.SymmetricCategory C} →
                        {comonObj' : (X : C) → CategoryTheory.ComonObj X} →
                          {isCommComonObj' : ∀ (X : C), CategoryTheory.IsCommComonObj X} →
                            {copy_tensor' :
                                autoParam
                                  (∀ (X Y : C),
                                    CategoryTheory.ComonObj.comul =
                                      CategoryTheory.CategoryStruct.comp
                                        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul
                                          CategoryTheory.ComonObj.comul)
                                        (CategoryTheory.MonoidalCategory.tensorμ X X Y Y))
                                  CategoryTheory.CopyDiscardCategory.copy_tensor._autoParam} →
                              {discard_tensor' :
                                  autoParam
                                    (∀ (X Y : C),
                                      CategoryTheory.ComonObj.counit =
                                        CategoryTheory.CategoryStruct.comp
                                          (CategoryTheory.MonoidalCategoryStruct.tensorHom
                                            CategoryTheory.ComonObj.counit CategoryTheory.ComonObj.counit)
                                          (CategoryTheory.MonoidalCategoryStruct.leftUnitor
                                              (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom)
                                    CategoryTheory.CopyDiscardCategory.discard_tensor._autoParam} →
                                {copy_unit' :
                                    autoParam
                                      (CategoryTheory.ComonObj.comul =
                                        (CategoryTheory.MonoidalCategoryStruct.leftUnitor
                                            (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv)
                                      CategoryTheory.CopyDiscardCategory.copy_unit._autoParam} →
                                  {discard_unit' :
                                      autoParam
                                        (CategoryTheory.ComonObj.counit =
                                          CategoryTheory.CategoryStruct.id
                                            (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                                        CategoryTheory.CopyDiscardCategory.discard_unit._autoParam} →
                                    { toSymmetricCategory := toSymmetricCategory, comonObj := comonObj,
                                          isCommComonObj := isCommComonObj, copy_tensor := copy_tensor,
                                          discard_tensor := discard_tensor, copy_unit := copy_unit,
                                          discard_unit := discard_unit } =
                                        { toSymmetricCategory := toSymmetricCategory', comonObj := comonObj',
                                          isCommComonObj := isCommComonObj', copy_tensor := copy_tensor',
                                          discard_tensor := discard_tensor', copy_unit := copy_unit',
                                          discard_unit := discard_unit' } →
                                      (toSymmetricCategory ≍ toSymmetricCategory' → comonObj ≍ comonObj' → P) → P

Defined in

Mathlib.CategoryTheory.CopyDiscardCategory.Basic

Cited by

0 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms