∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{u_4, u_1} D] {F G H : CategoryTheory.Functor D C}
  [CategoryTheory.Limits.HasPushouts C] (f : F ⟶ G) (g : F ⟶ H),
  CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)