{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      {J : Type u} →
        [inst_1 : CategoryTheory.Category.{v, u} J] →
          (D : CategoryTheory.Functor J T.Algebra) →
            CategoryTheory.Limits.Cone (D.comp T.forget) → CategoryTheory.Limits.Cone (D.comp T.forget)