∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {ι : Type u_3} {s : ι → C}
  [inst_1 : CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {α : Type} [Finite α]
  {f : α → ι}, CategoryTheory.Limits.HasBiproduct fun a => s (f a)