Lemma unelmodulefun_ismodulefun {R : ring} (M N : module R) : ismodulefun (λ x : M, (unel N)). Proof. use make_ismodulefun. - use make_isbinopfun. intros m m'. use pathsinv0. use lunax. - intros r m. rewrite module_mult_1. reflexivity. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids.