{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.MonoidalCategory C] →
        [CategoryTheory.MonoidalPreadditive C] →
          {X₁ Y₁ : C} →
            {f₁ : X₁ ⟶ Y₁} →
              CategoryTheory.Limits.CokernelCofork f₁ →
                {X₂ Y₂ : C} →
                  {f₂ : X₂ ⟶ Y₂} →
                    CategoryTheory.Limits.CokernelCofork f₂ →
                      [inst_4 :
                          CategoryTheory.Limits.HasBinaryCoproduct
                            (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₂)
                            (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ X₂)] →
                        CategoryTheory.Limits.CokernelCofork
                          (CategoryTheory.Limits.coprod.desc (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₁ Y₂)
                            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y₁ f₂))