{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X} →
      {inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀} →
        {P_1 : Sort u_2} →
          {trans : {i j : 𝒰.I₀} → (i ⟶ j) → (𝒰.X i ⟶ 𝒰.X j)} →
            {trans_id :
                autoParam
                  (∀ (i : 𝒰.I₀), trans (CategoryTheory.CategoryStruct.id i) = CategoryTheory.CategoryStruct.id (𝒰.X i))
                  AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_id._autoParam} →
              {trans_comp :
                  autoParam
                    (∀ {i j k : 𝒰.I₀} (hij : i ⟶ j) (hjk : j ⟶ k),
                      trans (CategoryTheory.CategoryStruct.comp hij hjk) =
                        CategoryTheory.CategoryStruct.comp (trans hij) (trans hjk))
                    AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_comp._autoParam} →
                {w :
                    autoParam
                      (∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (trans hij) (𝒰.f j) = 𝒰.f i)
                      AlgebraicGeometry.Scheme.Cover.LocallyDirected.w._autoParam} →
                  {directed :
                      ∀ {i j : 𝒰.I₀} (x : ↥(CategoryTheory.Limits.pullback (𝒰.f i) (𝒰.f j))),
                        ∃ k hki hkj y, (CategoryTheory.Limits.pullback.lift (trans hki) (trans hkj) ⋯) y = x} →
                    {property_trans :
                        autoParam (∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (trans hij))
                          AlgebraicGeometry.Scheme.Cover.LocallyDirected.property_trans._autoParam} →
                      {trans' : {i j : 𝒰.I₀} → (i ⟶ j) → (𝒰.X i ⟶ 𝒰.X j)} →
                        {trans_id' :
                            autoParam
                              (∀ (i : 𝒰.I₀),
                                trans' (CategoryTheory.CategoryStruct.id i) = CategoryTheory.CategoryStruct.id (𝒰.X i))
                              AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_id._autoParam} →
                          {trans_comp' :
                              autoParam
                                (∀ {i j k : 𝒰.I₀} (hij : i ⟶ j) (hjk : j ⟶ k),
                                  trans' (CategoryTheory.CategoryStruct.comp hij hjk) =
                                    CategoryTheory.CategoryStruct.comp (trans' hij) (trans' hjk))
                                AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_comp._autoParam} →
                            {w' :
                                autoParam
                                  (∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
                                    CategoryTheory.CategoryStruct.comp (trans' hij) (𝒰.f j) = 𝒰.f i)
                                  AlgebraicGeometry.Scheme.Cover.LocallyDirected.w._autoParam} →
                              {directed' :
                                  ∀ {i j : 𝒰.I₀} (x : ↥(CategoryTheory.Limits.pullback (𝒰.f i) (𝒰.f j))),
                                    ∃ k hki hkj y,
                                      (CategoryTheory.Limits.pullback.lift (trans' hki) (trans' hkj) ⋯) y = x} →
                                {property_trans' :
                                    autoParam (∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (trans' hij))
                                      AlgebraicGeometry.Scheme.Cover.LocallyDirected.property_trans._autoParam} →
                                  { trans := trans, trans_id := trans_id, trans_comp := trans_comp, w := w,
                                        directed := directed, property_trans := property_trans } =
                                      { trans := trans', trans_id := trans_id', trans_comp := trans_comp', w := w',
                                        directed := directed', property_trans := property_trans' } →
                                    (trans ≍ trans' → P_1) → P_1