Variation of `Functor.sum`

Stream: mathlib4

[Sina Hazratpour 𓃵]

Functor.sum defines a functor of type Sum A C ⥤ Sum B D. I need a variation which has the type Sum A B ⥤ C but I could not find it in CategoryTheory/Sums.

Actually, if we define

def sum₂ (F : A ⥤ C) (G : B ⥤ C) : Sum A B ⥤ C where

then we have that sum F G = sum₂ (F ⋙ Sum.inl_) (G ⋙ Sum.inr_).

So it seems to me that sum₂ is a bit more fundamental than sum the way it is defined.

Is it a good idea to add sum₂ to mathlib?

[Adam Topaz]

Are we really missing the (2-)universal property of docs#Sum ?

[Sina Hazratpour 𓃵]

I was not pursuing that path, since i thought I might get into problem with the universes (aka size issue). Are you suggesting defining sum₂ as a gap map out of the sum in the large 2-category of (small) categories?
I'll try this.

[Sina Hazratpour 𓃵]

@Adam Topaz
I think the situation is dual to docs#CategoryTheory.Functor.prod', might be a good idea to define Functor.sum'?