∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z)
  (g : Y ⟶ Z) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f],
  CategoryTheory.Limits.HasLimit
    (CategoryTheory.Limits.cospan
      (((CategoryTheory.Limits.cospan f g).comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace).map
        CategoryTheory.Limits.WalkingCospan.Hom.inl)
      (((CategoryTheory.Limits.cospan f g).comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace).map
        CategoryTheory.Limits.WalkingCospan.Hom.inr))