∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z),
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.pullbackConeOfLeftFst f g =
    { base := CategoryTheory.Limits.pullback.fst f.base g.base,
      c :=
        {
          app := fun U =>
            CategoryTheory.CategoryStruct.comp
              (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f (Opposite.unop U))
              (CategoryTheory.CategoryStruct.comp (g.c.app (Opposite.op (⋯.functor.obj (Opposite.unop U))))
                (Y.presheaf.map (CategoryTheory.eqToHom ⋯))),
          naturality := ⋯ } }