Commit 2020-04-12 20:36 ef4d2354

feat(category_theory): biproducts, and biproducts in AddCommGroup (#2187) This PR

1. 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.
2. 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)
3. because these custom instances have identical underlying objects, it's trivial to put them together to get a has_biproducts AddCommGroup.
4. as for 2 & 3 with binary biproducts for AddCommGroup, implemented simply as the cartesian group.