The category of abelian groups has finite biproducts #
We verify that the biproduct in AddCommGroup is isomorphic to
the cartesian product of the underlying types:
The map from an arbitrary cone over a indexed family of abelian groups
to the cartesian product of those groups.
We verify that the biproduct we've just defined is isomorphic to the AddCommGroup structure
on the dependent function type