{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {P : Sort u_1} →
        {toCopyDiscardCategory : CategoryTheory.CopyDiscardCategory C} →
          {discard_natural :
              ∀ {X Y : C} (f : X ⟶ Y),
                CategoryTheory.CategoryStruct.comp f CategoryTheory.ComonObj.counit = CategoryTheory.ComonObj.counit} →
            {toCopyDiscardCategory' : CategoryTheory.CopyDiscardCategory C} →
              {discard_natural' :
                  ∀ {X Y : C} (f : X ⟶ Y),
                    CategoryTheory.CategoryStruct.comp f CategoryTheory.ComonObj.counit =
                      CategoryTheory.ComonObj.counit} →
                { toCopyDiscardCategory := toCopyDiscardCategory, discard_natural := discard_natural } =
                    { toCopyDiscardCategory := toCopyDiscardCategory', discard_natural := discard_natural' } →
                  (toCopyDiscardCategory ≍ toCopyDiscardCategory' → P) → P