∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  {X Y : AlgebraicGeometry.PresheafedSpace C} (α : X ≅ Y) (x : ↑↑X),
  CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap α.hom x)