∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  [CategoryTheory.HasSheafify J (Type u)], CategoryTheory.IsRegularEpiCategory (CategoryTheory.Sheaf J (Type u))