∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X}
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] (trans trans_1 : {i j : 𝒰.I₀} → (i ⟶ j) → (𝒰.X i ⟶ 𝒰.X j))
  (e_trans : trans = trans_1)
  (trans_id : ∀ (i : 𝒰.I₀), trans (CategoryTheory.CategoryStruct.id i) = CategoryTheory.CategoryStruct.id (𝒰.X i))
  (trans_comp :
    ∀ {i j k : 𝒰.I₀} (hij : i ⟶ j) (hjk : j ⟶ k),
      trans (CategoryTheory.CategoryStruct.comp hij hjk) = CategoryTheory.CategoryStruct.comp (trans hij) (trans hjk))
  (w : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), CategoryTheory.CategoryStruct.comp (trans hij) (𝒰.f j) = 𝒰.f i)
  (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 : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (trans hij)),
  { trans := trans, trans_id := trans_id, trans_comp := trans_comp, w := w, directed := directed,
      property_trans := property_trans } =
    { trans := trans_1, trans_id := ⋯, trans_comp := ⋯, w := ⋯, directed := ⋯, property_trans := ⋯ }