Definition quotmod_ringfun : ringfun R (ringofendabgr quotmod_abgr). Proof. unfold ringfun, rigfun. use rigfunconstr. - exact quotmod_ringmap. - use make_isrigfun. all: use make_ismonoidfun; [ use make_isbinopfun; intros r r' | ]. all: use monoidfun_paths; use funextfun. all: use (setquotunivprop E (λ m, make_hProp _ _)); [use isasetsetquot|]. all: intros m; simpl; unfold unel, quotmod_ringact. all: [> do 3 rewrite (setquotunivcomm E) | rewrite (setquotunivcomm E) | do 3 rewrite (setquotunivcomm E) | rewrite (setquotunivcomm E)]. all: use maponpaths; simpl. + use module_mult_is_rdistr. + use module_mult_0_to_0. + use module_mult_assoc. + use module_mult_unel2. 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.