{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {motive : CategoryTheory.CopyDiscardCategory C → Sort u_1} →
        ([toSymmetricCategory : CategoryTheory.SymmetricCategory C] →
            [comonObj : (X : C) → CategoryTheory.ComonObj X] →
              [isCommComonObj : ∀ (X : C), CategoryTheory.IsCommComonObj X] →
                (copy_tensor :
                    ∀ (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)) →
                  (discard_tensor :
                      ∀ (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) →
                    (copy_unit :
                        CategoryTheory.ComonObj.comul =
                          (CategoryTheory.MonoidalCategoryStruct.leftUnitor
                              (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv) →
                      (discard_unit :
                          CategoryTheory.ComonObj.counit =
                            CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) →
                        motive
                          { toSymmetricCategory := toSymmetricCategory, comonObj := comonObj,
                            isCommComonObj := isCommComonObj, copy_tensor := copy_tensor,
                            discard_tensor := discard_tensor, copy_unit := copy_unit, discard_unit := discard_unit }) →
          (t : CategoryTheory.CopyDiscardCategory C) → motive t