Definition multimodule_struct {I : UU} {rings : I -> ring} {G : abgr} (structs : ∏ i : I, module_struct (rings i) G) := ∏ (i1 i2 : I) (ne : (i1 = i2) -> hfalse), arecompatibleactions (structs i1) (structs i2).
Require Import UniMath.Algebra.Modules.Core. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Foundations.Preamble. Require Import UniMath.Foundations.Sets.