mathlib

ff84bf47 - feat(category_theory/monad/limits): forgetful creates colimits (#2138)

feat(category_theory/monad/limits): forgetful creates colimits (#2138) * forgetful creates colimits * tidy up proofs * add docs * suggestions from review Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>