{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {inst : P.IsStableUnderBaseChange} →
    {S : AlgebraicGeometry.Scheme} →
      {J : Type u_1} →
        {inst_1 : CategoryTheory.Category.{v_1, u_1} J} →
          {D : CategoryTheory.Functor J (P.Over ⊤ S)} →
            {𝒰 : S.OpenCover} →
              {inst_2 : CategoryTheory.Category.{v_3, u_2} 𝒰.I₀} →
                {inst_3 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰} →
                  [⦃X Y : AlgebraicGeometry.Scheme⦄ → (x : X ⟶ Y) → SizeOf (P x)] →
                    [SizeOf J] → AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰 → ℕ