∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (𝒰.f x))
      (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x)) (𝒰.f y))