Lemma moduleiso_z_iso (M N : ob mod_category) : moduleiso M N -> z_iso M N. Proof. intro f. use make_z_iso'. - exact (moduleiso_to_modulefun f). - exact (moduleiso_is_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.