Definition quotmod_ringmap : R -> ringofendabgr quotmod_abgr. Proof. intros r. use tpair. + exact (quotmod_ringact r). + use make_ismonoidfun. * use make_isbinopfun. use (setquotuniv2prop E (λ a b, make_hProp _ _)); [use isasetsetquot|]. intros m m'. unfold quotmod_ringact, setquotfun2; rewrite (setquotunivcomm E), (setquotunivcomm E); simpl; unfold setquotfun2; rewrite (setquotuniv2comm E), (setquotuniv2comm E), (setquotunivcomm E). apply weqpathsinsetquot. assert (H : r * (m + m') = r * m + r * m') by use module_mult_is_ldistr. simpl in H; rewrite H. use eqrelrefl. * unfold unel, quotmod_ringact; simpl; rewrite (setquotunivcomm E). apply maponpaths. apply module_mult_1. Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Modules.Core. Require Import UniMath.Algebra.Modules.Submodule.