Coproduct presentation for monad algebras (source code)

= Coproduct presentation for monad algebras

For <algebras for a monad> $(A,\alpha),(B,\beta)$ and underlying binary <coproducts in a category>, put $\kappa=[T\nu_1,T\nu_2]:TA+TB\to T(A+B)$. If the algebra pair $F(\alpha+\beta),\mu_{A+B}F\kappa:F(TA+TB)\rightrightarrows F(A+B)$ has a <coequalizer>, that coequalizer is their algebra coproduct. An algebra map from $F(A+B)$ transposes to $[a,b]:A+B\to C$; equalizing the pair is exactly the two algebra-morphism equations for $a,b$. The pair is reflexive through $F(\eta_A+\eta_B)$.