∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  AlgebraicGeometry.Scheme.Hom.appIso (CategoryTheory.CategoryStruct.id X) U =
    CategoryTheory.Functor.mapIso X.presheaf (CategoryTheory.eqToIso ⋯).op