Lemma isaproparecompatibleactions {R S G} (mr : module_struct R G) (ms : module_struct S G) : isaprop (arecompatibleactions mr ms). Proof. apply (impredtwice 1); intros r s. apply (isofhlevelweqb 1 (Y := (module_mult (G,, mr) r ∘ module_mult (G,, ms) s ~ module_mult (G,, ms) s ∘ module_mult (G,, mr) r))). apply invweq. apply weqfunextsec. apply (impred 1); intros x. apply (pr2 (pr1 (pr1 G))). 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.