{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (homGroup : autoParam ((P Q : C) → AddCommGroup (P ⟶ Q)) CategoryTheory.Preadditive.homGroup._autoParam) →
      (add_comp :
          autoParam
            (∀ (P Q R : C) (f f' : P ⟶ Q) (g : Q ⟶ R),
              CategoryTheory.CategoryStruct.comp (f + f') g =
                CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f' g)
            CategoryTheory.Preadditive.add_comp._autoParam) →
        (comp_add :
            autoParam
              (∀ (P Q R : C) (f : P ⟶ Q) (g g' : Q ⟶ R),
                CategoryTheory.CategoryStruct.comp f (g + g') =
                  CategoryTheory.CategoryStruct.comp f g + CategoryTheory.CategoryStruct.comp f g')
              CategoryTheory.Preadditive.comp_add._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_finite_products : CategoryTheory.Limits.HasFiniteProducts C] →
                [has_kernels : CategoryTheory.Limits.HasKernels C] →
                  [has_cokernels : CategoryTheory.Limits.HasCokernels C] → CategoryTheory.Abelian C