∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) {x y : ↑↑X} (h : x ⤳ y),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯)
      (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f y)
      (X.presheaf.stalkSpecializes h)