Combine coproducts

Stream: Is there code for X?

[Christian Merten]

Is there something like this:

import Mathlib

open CategoryTheory Limits Functor

variable {C : Type u} [Category.{v, u} C]

def comb (α : Type*) (f : α → Type*) (g : (a : α) → f a → C)
    (t : ∀ a, ColimitCocone (Discrete.functor (g a)))
    (s : ColimitCocone (Discrete.functor (fun a ↦ (t a).cocone.pt))) :
    Cocone (Discrete.functor (Sigma.uncurry g : Sigma f → C)) := sorry

i.e. given a family of coproduct diagrams indexed over some type α and a coproduct of the cone points, is there one big coproduct on Sigma f?
I tried to formulate this for arbitrary functors first (indead of restricting to Discrete.functor) but I struggled to emulate the dependence on the value of f.
There is docs#CategoryTheory.Limits.combineCocones but there the index categories are the same for every diagram (i.e. f above would have to be constant).

[Joël Riou]

I prove something similar in PR #8242:
https://github.com/leanprover-community/mathlib4/pull/8242/files#diff-872c679954b062c45a489c6ba4184c58b3220532467f779d8859dcc80692358dR435-R444