Sort u →
  {ι : Type u_1} →
    {A : ι → Type u_2} →
      [inst : AddMonoid ι] →
        [inst_1 : (i : ι) → AddCommMonoid (A i)] →
          DirectSum.GSemiring A →
            {ι' : Type u_1} →
              {A' : ι' → Type u_2} →
                [inst' : AddMonoid ι'] → [inst'_1 : (i : ι') → AddCommMonoid (A' i)] → DirectSum.GSemiring A' → Sort u