∀ {J : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] [inst_2 : Small.{u_1, u_3} J]
  (j k : Shrink.{u_1, u_3} J),
  AlgebraicGeometry.IsOpenImmersion
    (AlgebraicGeometry.Scheme.IsLocallyDirected.V F ((equivShrink J).symm j) ((equivShrink J).symm k)).ι