Definition modules_univalence_weq (M N : mod_category) : (M ╝ N) ≃ (moduleiso' M N). Proof. use weqbandf. - apply abgr_univalence. - intro e. use invweq. induction M. induction N. cbn in e. induction e. use weqimplimpl. + intro i. use total2_paths2_f. * use funextfun. intro r. use total2_paths2_f. apply funextfun. intro x. exact (i r x). apply isapropismonoidfun. * apply isapropisrigfun. + intro i. cbn. intros r x. unfold idmonoidiso. cbn in i. induction i. apply idpath. + apply isapropislinear. + apply isasetrigfun. 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.