proposition: Lemma moduleiso_is_z_iso {M N : ob mod_category} (f : moduleiso M N) : @is_z_isomorphism _ M N (moduleiso_to_modulefun f).
proof: Proof. exists (make_modulefun (invmoduleiso f) (pr2 (invmoduleiso f))). split; use total2_paths_f. + apply funextfun. intro. apply homotinvweqweq. + apply isapropismodulefun. + apply funextfun. intro. apply homotweqinvweq. + apply isapropismodulefun. Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.Algebra.Modules UniMath.Algebra.Modules.Examples UniMath.CategoryTheory.Limits.Zero