∀ {C₁ : Type u_6} {C₂ : Type u_4} {C₃ : Type u_2} [inst : CategoryTheory.Category.{u_5, u_6} C₁]
  [inst_1 : CategoryTheory.Category.{u_3, u_4} C₂] [inst_2 : CategoryTheory.Category.{u_1, u_2} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) [CategoryTheory.Limits.HasPushouts C₃]
  (f₁ : CategoryTheory.Arrow C₁) (f₂ : CategoryTheory.Arrow C₂),
  CategoryTheory.Limits.HasColimit
    (CategoryTheory.Limits.span ((F.map f₁.hom).app ((CategoryTheory.Functor.id C₂).obj f₂.left))
      ((F.obj ((CategoryTheory.Functor.id C₁).obj f₁.left)).map f₂.hom))