Module biproducts with a universe-polymorphic index

Mathlib's explicit ModuleCat.biproductIsoPi specializes its finite index to Type. This variant uses the already universe-polymorphic product cone.

noncomputable def MagnitudeConjecture.ModuleCat.biproductIsoPi {R : Type u} [Ring R] {J : Type w} (f : J → ModuleCat R) [Finite J] : ⨁ f ≅ ModuleCat.of R ((j : J) → ↑(f j))

A finite categorical biproduct of modules is the dependent function module, with no restriction on the universe of the finite index.