proposition: Lemma moduleisweq_z_iso {M N : ob mod_category} (f : z_iso M N) : isweq (pr1modulefun (morphism_from_z_iso _ _ f)).
proof: Proof. use (isweq_iso (pr1modulefun (morphism_from_z_iso _ _ f))). - exact (pr1modulefun (inv_from_z_iso f)). - intro; set (T:= z_iso_inv_after_z_iso f). apply subtypeInjectivity in T. + apply (toforallpaths _ _ _ T). + intro; apply isapropismodulefun. - intro; set (T:= z_iso_after_z_iso_inv f). apply subtypeInjectivity in T. + apply (toforallpaths _ _ _ T). + intro; 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