Convert from monad (i.e. Lean's Type-based monads) to category_theory.monad
This allows us to use these monads in category theory.
@[instance]
Equations
- category_theory.category_theory.monad m = {η := {app := has_pure.pure applicative.to_has_pure, naturality' := _}, μ := {app := mjoin _inst_1, naturality' := _}, assoc' := _, left_unit' := _, right_unit' := _}