{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      (A : C) →
        (a : T.obj A ⟶ A) →
          autoParam (CategoryTheory.CategoryStruct.comp (T.η.app A) a = CategoryTheory.CategoryStruct.id A)
              CategoryTheory.Monad.Algebra.unit._autoParam →
            autoParam
                (CategoryTheory.CategoryStruct.comp (T.μ.app A) a = CategoryTheory.CategoryStruct.comp (T.map a) a)
                CategoryTheory.Monad.Algebra.assoc._autoParam →
              T.Algebra