{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Comonad C} →
      [CategoryTheory.Limits.PreservesLimitsOfSize.{v, u, v₁, v₁, u₁, u₁} T.toFunctor] →
        CategoryTheory.CreatesLimitsOfSize.{v, u, v₁, v₁, max u₁ v₁, u₁} T.forget