∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [CategoryTheory.Limits.HasImages C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] {A : C} (f g : CategoryTheory.MonoOver A),
  CategoryTheory.Limits.HasImage
    ((CategoryTheory.Functor.uncurry.obj CategoryTheory.Over.coprod).obj
        (((CategoryTheory.MonoOver.forget A).prod (CategoryTheory.MonoOver.forget A)).obj (f, g))).hom