∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {S : AlgebraicGeometry.Scheme} {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J]
  (F : CategoryTheory.Functor J (P.Over ⊤ S))
  [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f).left]
  [(F.comp
        ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp
          ((CategoryTheory.Over.forget S).comp AlgebraicGeometry.Scheme.forget))).IsLocallyDirected]
  [Quiver.IsThin J] [Small.{u, u_1} J], CategoryTheory.Limits.HasColimit F