∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f], IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f.hom.base)