Lemma moduleiso_is_z_iso {M N : ob mod_category} (f : moduleiso M N) : @is_z_isomorphism _ M N (moduleiso_to_modulefun f). 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.
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.