Biproduct-induced addition of morphisms (source code)

= Biproduct-induced addition of morphisms
{title2=$f+g=\nabla_B\langle f,g\rangle$}

In a <pointed category> with finite <product in a category> and <coproducts in a category> and invertible canonical maps $c:A+B\to A\times B$, the unique <commutative-monoid enrichment> is $f+g=[1_B,1_B]c_{B,B}^{-1}\langle f,g\rangle$. Associativity and commutativity follow by comparing fold maps on triple and swapped coproduct injections. Composition distributes by the universal properties. For uniqueness, bilinearity forces $i_1p_1+i_2p_2=1$ on each biproduct, and composing with the fold and the paired morphism forces the addition formula.