Definition quotmoduniv (N : module R) (f : R-mod(M, N)) (is : iscomprelfun E f) : R-mod(quotmod, N). Proof. use make_modulefun. - now use (setquotuniv E _ f). - use make_ismodulefun. + use make_isbinopfun. use (setquotuniv2prop E (λ m n, make_hProp _ _)); [use isasetmodule|]. intros m m'. simpl. unfold op, setquotfun2. rewrite setquotuniv2comm. do 3 rewrite (setquotunivcomm E). apply modulefun_to_isbinopfun. + intros r. use (setquotunivprop E (λ m, make_hProp _ _)); [use isasetmodule|]. intros m. assert (H : r * quotmod_quotmap m = quotmod_quotmap (r * m)) by use (! modulefun_to_islinear _ _ _). simpl in H. simpl. rewrite H. do 2 rewrite (setquotunivcomm E). apply modulefun_to_islinear. 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.