Commit 2020-12-15 10:30 8041945f

View on Github →

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.

Estimated changes