∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.QuasiSeparated f],
  CategoryTheory.NatTrans.Coequifibered
    ((AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor Y).op.whiskerLeft
      (AlgebraicGeometry.Scheme.Hom.normalizationDiagramMap f))