Lemma moduleiso'_to_moduleisweq_iso {R} (M N : module R) : isweq (moduleiso'_to_moduleiso M N). Proof. use (isweq_iso _ (moduleiso_to_moduleiso' M N)). - intro w. unfold moduleiso'_to_moduleiso, moduleiso_to_moduleiso'. cbn. induction w as [w1 w2]; cbn. use total2_paths_f; cbn. * use total2_paths_f; cbn. + reflexivity. + apply isapropismonoidfun. * apply isapropislinear. - reflexivity. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids.