feat(category_theory/monad): monadicity theorems (#5137)
This is a proof of the reflexive (or crude) monadicity theorem along with a complete proof of Beck's monadicity theorem.
Also renames the prefix for special monad coequalizers to `free_coequalizer` rather than `coequalizer`, to avoid name-clashes when both `monad` and `limits` are imported.
