∀ {R : Type (max u_2 u_3 u_1)} [inst : CommRing R] {D : Type u_3} [inst_1 : CategoryTheory.SmallCategory D]
  {E : Type u_1} [inst_2 : CategoryTheory.SmallCategory E] (I' : CategoryTheory.Functor E D)
  (I : CategoryTheory.Functor D (Ideal R)) (i : ℕ),
  CategoryTheory.Limits.HasColimit (localCohomology.diagram (I'.comp I) i)