Commit 2020-12-04 07:42 240f6eb9
View on Github →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