Definition mod_category_idtoisweq_z_iso : ∏ M N : mod_category, isweq (fun p : M = N => idtoiso p). Proof. intros M N. use (isweqhomot (weqcomp (modules_univalence M N) (moduleiso_weq_z_iso M N)) _). - intro p. induction p. use (pathscomp0 weqcomp_to_funcomp_app). cbn. use total2_paths_f. + apply idpath. + apply (isaprop_is_z_isomorphism (identity M)). - apply weqproperty. 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.