feat(category_theory/monad): cleanups in monad algebra (#5193)
- Converts the simp normal form for composition of algebra homs to use category notation.
- Adds simps where appropriate
- Golfs proofs, remove some erw and nonterminal simps
- Remove some redundant brackets
