feat(category_theory): preadditive binary biproducts (#2747)
This PR introduces "preadditive binary biproducts", which correspond to the second definition of biproducts given in #2177.
* Preadditive binary biproducts are binary biproducts.
* In a preadditive category, a binary product is a preadditive binary biproduct.
* This directly implies that `AddCommGroup` has preadditive binary biproducts. The existence of binary coproducts in `AddCommGroup` is then a consequence of abstract nonsense.
