{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {motive : CategoryTheory.CopyDiscardCategory C → Sort u_1} →
        (t : CategoryTheory.CopyDiscardCategory C) →
          ([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 }) →
            motive t