∀ {C₁ : Type u_6} {C₂ : Type u_2} {C₃ : Type u_4} [inst : CategoryTheory.Category.{u_5, u_6} C₁]
  [inst_1 : CategoryTheory.Category.{u_1, u_2} C₂] [inst_2 : CategoryTheory.Category.{u_3, u_4} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) (X₁ : CategoryTheory.Arrow C₁)
  [CategoryTheory.Limits.HasPullbacks C₂] [inst_4 : CategoryTheory.Limits.HasPushouts C₃]
  (X₂ : CategoryTheory.Arrow C₂),
  CategoryTheory.Limits.HasLimit
    (CategoryTheory.Limits.cospan
      ((G.obj (Opposite.op ((CategoryTheory.Functor.id C₁).obj (Opposite.unop (Opposite.op X₁)).left))).map
        ((F.leibnizPushout.obj X₁).obj X₂).hom)
      ((G.map (Opposite.unop (Opposite.op X₁)).hom.op).app
        ((CategoryTheory.Functor.id C₃).obj ((F.leibnizPushout.obj X₁).obj X₂).right)))