{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {motive : CategoryTheory.Monad C → Sort u} →
      ((toFunctor : CategoryTheory.Functor C C) →
          (η : CategoryTheory.Functor.id C ⟶ toFunctor) →
            (μ : toFunctor.comp toFunctor ⟶ toFunctor) →
              (assoc :
                  ∀ (X : C),
                    CategoryTheory.CategoryStruct.comp (toFunctor.map (μ.app X)) (μ.app X) =
                      CategoryTheory.CategoryStruct.comp (μ.app (toFunctor.obj X)) (μ.app X)) →
                (left_unit :
                    ∀ (X : C),
                      CategoryTheory.CategoryStruct.comp (η.app (toFunctor.obj X)) (μ.app X) =
                        CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj (toFunctor.obj X))) →
                  (right_unit :
                      ∀ (X : C),
                        CategoryTheory.CategoryStruct.comp (toFunctor.map (η.app X)) (μ.app X) =
                          CategoryTheory.CategoryStruct.id (toFunctor.obj ((CategoryTheory.Functor.id C).obj X))) →
                    motive
                      { toFunctor := toFunctor, η := η, μ := μ, assoc := assoc, left_unit := left_unit,
                        right_unit := right_unit }) →
        (t : CategoryTheory.Monad C) → motive t