Lemma z_iso_moduleiso (M N : ob mod_category) : z_iso M N -> moduleiso M N. Proof. intro f. use make_moduleiso. - use make_weq. + exact (pr1modulefun (morphism_from_z_iso _ _ f)). + exact (moduleisweq_z_iso f). - exact (modulefun_ismodulefun (morphism_from_z_iso _ _ f)). Defined.
Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.Algebra.Modules. Require Import UniMath.Algebra.Modules.Examples. Require Import UniMath.CategoryTheory.Limits.Zero.