{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 𝒰} →
                  {P_1 : Sort u_3} →
                    {cocone :
                        (i : 𝒰.I₀) →
                          CategoryTheory.Limits.Cocone
                            (D.comp (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)))} →
                      {isColimit : (i : 𝒰.I₀) → CategoryTheory.Limits.IsColimit (cocone i)} →
                        {prop_trans : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij)} →
                          {cocone' :
                              (i : 𝒰.I₀) →
                                CategoryTheory.Limits.Cocone
                                  (D.comp (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)))} →
                            {isColimit' : (i : 𝒰.I₀) → CategoryTheory.Limits.IsColimit (cocone' i)} →
                              {prop_trans' :
                                  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij)} →
                                { cocone := cocone, isColimit := isColimit, prop_trans := prop_trans } =
                                    { cocone := cocone', isColimit := isColimit', prop_trans := prop_trans' } →
                                  (cocone ≍ cocone' → isColimit ≍ isColimit' → P_1) → P_1