Definition mult_to_module_struct {R : ring} {G : abgr} {m : R -> G -> G} (ax1 : mult_isldistr_wrt_grop m) (ax2 : mult_isrdistr_wrt_ringop1 m) (ax3 : mult_isrdistr_wrt_ringop2 m) (ax4 : mult_unel m) : module_struct R G. Proof. split with (λ r : R, mult_to_ringofendabgr ax1 r). apply make_dirprod. - apply make_dirprod. + intros r s. use total2_paths2_f. * apply funextfun. intro x. apply ax2. * apply isapropismonoidfun. + use total2_paths2_f. * apply funextfun. intro x. change (m ringunel1 x = unel G). apply (grlcan G (m (ringunel1) x)). rewrite runax. rewrite <- (ax2 ringunel1 ringunel1 x). rewrite ringrunax1. apply idpath. * apply isapropismonoidfun. - apply make_dirprod. + intros r s. use total2_paths2_f. * apply funextfun. intro x. apply ax3. * apply isapropismonoidfun. + use total2_paths2_f. * apply funextfun. intro x. apply ax4. * apply isapropismonoidfun. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids.