∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Limits.FormalCoproduct C}
  (f : (CategoryTheory.Limits.FormalCoproduct.incl C).obj X ⟶ Y),
  CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl (CategoryTheory.Limits.FormalCoproduct.Hom.asSigma f).fst
      (CategoryTheory.Limits.FormalCoproduct.Hom.asSigma f).snd =
    f