{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z S T : C} →
      (f₁ : S ⟶ W) →
        (f₂ : S ⟶ X) →
          [inst_1 : CategoryTheory.Limits.HasPushout f₁ f₂] →
            (g₁ : T ⟶ Y) →
              (g₂ : T ⟶ Z) →
                [inst_2 : CategoryTheory.Limits.HasPushout g₁ g₂] →
                  (i₁ : W ⟶ Y) →
                    (i₂ : X ⟶ Z) →
                      (i₃ : S ⟶ T) →
                        CategoryTheory.CategoryStruct.comp f₁ i₁ = CategoryTheory.CategoryStruct.comp i₃ g₁ →
                          CategoryTheory.CategoryStruct.comp f₂ i₂ = CategoryTheory.CategoryStruct.comp i₃ g₂ →
                            (CategoryTheory.Limits.pushout f₁ f₂ ⟶ CategoryTheory.Limits.pushout g₁ g₂)