∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (k : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (𝒰.f k) (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (𝒰.X k)) (𝒰.f k)