{C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {P : Sort u} →
      {toFunctor : CategoryTheory.Functor C C} →
        {η : CategoryTheory.Functor.id C ⟶ toFunctor} →
          {μ : toFunctor.comp toFunctor ⟶ toFunctor} →
            {assoc :
                autoParam
                  (∀ (X : C),
                    CategoryTheory.CategoryStruct.comp (toFunctor.map (μ.app X)) (μ.app X) =
                      CategoryTheory.CategoryStruct.comp (μ.app (toFunctor.obj X)) (μ.app X))
                  CategoryTheory.Monad.assoc._autoParam} →
              {left_unit :
                  autoParam
                    (∀ (X : C),
                      CategoryTheory.CategoryStruct.comp (η.app (toFunctor.obj X)) (μ.app X) =
                        CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj (toFunctor.obj X)))
                    CategoryTheory.Monad.left_unit._autoParam} →
                {right_unit :
                    autoParam
                      (∀ (X : C),
                        CategoryTheory.CategoryStruct.comp (toFunctor.map (η.app X)) (μ.app X) =
                          CategoryTheory.CategoryStruct.id (toFunctor.obj ((CategoryTheory.Functor.id C).obj X)))
                      CategoryTheory.Monad.right_unit._autoParam} →
                  {toFunctor' : CategoryTheory.Functor C C} →
                    {η' : CategoryTheory.Functor.id C ⟶ toFunctor'} →
                      {μ' : toFunctor'.comp toFunctor' ⟶ toFunctor'} →
                        {assoc' :
                            autoParam
                              (∀ (X : C),
                                CategoryTheory.CategoryStruct.comp (toFunctor'.map (μ'.app X)) (μ'.app X) =
                                  CategoryTheory.CategoryStruct.comp (μ'.app (toFunctor'.obj X)) (μ'.app X))
                              CategoryTheory.Monad.assoc._autoParam} →
                          {left_unit' :
                              autoParam
                                (∀ (X : C),
                                  CategoryTheory.CategoryStruct.comp (η'.app (toFunctor'.obj X)) (μ'.app X) =
                                    CategoryTheory.CategoryStruct.id
                                      ((CategoryTheory.Functor.id C).obj (toFunctor'.obj X)))
                                CategoryTheory.Monad.left_unit._autoParam} →
                            {right_unit' :
                                autoParam
                                  (∀ (X : C),
                                    CategoryTheory.CategoryStruct.comp (toFunctor'.map (η'.app X)) (μ'.app X) =
                                      CategoryTheory.CategoryStruct.id
                                        (toFunctor'.obj ((CategoryTheory.Functor.id C).obj X)))
                                  CategoryTheory.Monad.right_unit._autoParam} →
                              { toFunctor := toFunctor, η := η, μ := μ, assoc := assoc, left_unit := left_unit,
                                    right_unit := right_unit } =
                                  { toFunctor := toFunctor', η := η', μ := μ', assoc := assoc', left_unit := left_unit',
                                    right_unit := right_unit' } →
                                (toFunctor ≍ toFunctor' → η ≍ η' → μ ≍ μ' → P) → P