feat(category_theory/monad): algebras for the coproduct monad (#5679)
WIP, I'll fix it up when the dependent PRs merge
<!--
put comments you want to keep out of the PR commit here.
If this PR depends on other PRs, please list them below this comment,
using the following format:
- [ ] depends on: #abc [optional extra text]
- [ ] depends on: #xyz [optional extra text]
-->
- [x] depends on: #5674
- [x] depends on: #5677
- [x] depends on: #5678