{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          {S X : C} →
            (πX : X ⟶ S) →
              [inst_1 :
                  CategoryTheory.Limits.HasColimitsOfShape
                    (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] →
                [inst_2 :
                    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
                      (CategoryTheory.SmallObject.functorObjLeft f πX)] →
                  X ⟶ CategoryTheory.SmallObject.functorObj f πX