Convert from
monad
(i.e. Lean's
Type
-based monads) to
category_theory.monad
This allows us to use these monads in category theory.