proposition: Lemma moduleiso_isweq_z_iso (M N : ob mod_category) : isweq (@moduleiso_z_iso M N).
proof: Proof. apply (isweq_iso _ (z_iso_moduleiso M N)). - intro. apply subtypePath. + intro; apply isapropismodulefun. + unfold moduleiso_z_iso, z_iso_moduleiso. use total2_paths_f. * apply idpath. * apply isapropisweq. - intro; unfold z_iso_moduleiso, moduleiso_z_iso. use total2_paths_f. + apply idpath. + apply isaprop_is_z_isomorphism. 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