{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [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) →
          (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f], Nonempty (CategoryTheory.NormalMono f)) →
            (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f], Nonempty (CategoryTheory.NormalEpi f)) →
              [has_zero_object : CategoryTheory.Limits.HasZeroObject C] →
                [has_kernels : CategoryTheory.Limits.HasKernels C] →
                  [has_cokernels : CategoryTheory.Limits.HasCokernels C] →
                    [has_finite_products : CategoryTheory.Limits.HasFiniteProducts C] →
                      [has_finite_coproducts : CategoryTheory.Limits.HasFiniteCoproducts C] →
                        CategoryTheory.NonPreadditiveAbelian C