# Commit 2020-04-12 20:36 ef4d2354

View on Github →feat(category_theory): biproducts, and biproducts in AddCommGroup (#2187) This PR

- adds typeclasses
`has_biproducts`

(implicitly restricting to finite biproducts, which is the only interesting case) and`has_binary_biproducts`

, and the usual tooling for special shapes of limits. - provides customised
`has_products`

and`has_coproducts`

instances for`AddCommGroup`

, which are both just dependent functions (for`has_coproducts`

we have to assume the indexed type is finite and decidable) - because these custom instances have identical underlying objects, it's trivial to put them together to get a
`has_biproducts AddCommGroup`

. - as for 2 & 3 with binary biproducts for AddCommGroup, implemented simply as the cartesian group.