Lemma isapropmultimodule_struct {I : UU} {rings : I -> ring} {G : abgr} (structs : ∏ i : I, module_struct (rings i) G) : isaprop (multimodule_struct structs). Proof. apply (impredtwice 1); intros i1 i2. apply impredfun. apply isaproparecompatibleactions. Defined.
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.