∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  CategoryTheory.CategoryStruct.comp hU.isoSpec.inv U.toSpecΓ =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U)))