Lemma moduleiso_isweq_z_iso (M N : ob mod_category) : isweq (@moduleiso_z_iso M N). 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.
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.