Lemma moduleisweq_z_iso {M N : ob mod_category} (f : z_iso M N) : isweq (pr1modulefun (morphism_from_z_iso _ _ f)). 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.
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.