{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {P : Sort u_1} →
      {zero : (X Y : C) → Zero (X ⟶ Y)} →
        {comp_zero :
            autoParam (∀ {X Y : C} (f : X ⟶ Y) (Z : C), CategoryTheory.CategoryStruct.comp f 0 = 0)
              CategoryTheory.Limits.HasZeroMorphisms.comp_zero._autoParam} →
          {zero_comp :
              autoParam (∀ (X : C) {Y Z : C} (f : Y ⟶ Z), CategoryTheory.CategoryStruct.comp 0 f = 0)
                CategoryTheory.Limits.HasZeroMorphisms.zero_comp._autoParam} →
            {zero' : (X Y : C) → Zero (X ⟶ Y)} →
              {comp_zero' :
                  autoParam (∀ {X Y : C} (f : X ⟶ Y) (Z : C), CategoryTheory.CategoryStruct.comp f 0 = 0)
                    CategoryTheory.Limits.HasZeroMorphisms.comp_zero._autoParam} →
                {zero_comp' :
                    autoParam (∀ (X : C) {Y Z : C} (f : Y ⟶ Z), CategoryTheory.CategoryStruct.comp 0 f = 0)
                      CategoryTheory.Limits.HasZeroMorphisms.zero_comp._autoParam} →
                  { zero := zero, comp_zero := comp_zero, zero_comp := zero_comp } =
                      { zero := zero', comp_zero := comp_zero', zero_comp := zero_comp' } →
                    (zero ≍ zero' → P) → P