# Commit 2020-06-18 20:37 21bf8737

View on Github →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:

- we don't provide the instances from
`has_finite_biproducts`

to`has_finite_(co)products`

- we don't define the preadditive version of finite biproducts (we only did the binary ones)
- 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.