{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {P : Sort u_1} →
      {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} →
            {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} →
                  { homGroup := homGroup, add_comp := add_comp, comp_add := comp_add } =
                      { homGroup := homGroup', add_comp := add_comp', comp_add := comp_add' } →
                    (homGroup ≍ homGroup' → P) → P