Commit 2020-06-18 20:37 21bf8737

refactor(category_theory/abelian): use has_finite_products (#2917) This doesn't go nearly as far as I wanted. Really I'd like to factor out additive, which is a preadditive category with all finite biproducts, and then layer abelian on top of that (with (co)kernels and every epi/mono normal). I can't do that immediately, because:

1. we don't provide the instances from has_finite_biproducts to has_finite_(co)products
2. we don't define the preadditive version of finite biproducts (we only did the binary ones)
3. hence we don't show that in a preadditive category finite products give rise to finite biproducts @TwoFX, @b-mehta, if either of you are interested in doing any of these, that would be great. I'll hopefully get to them eventually.