Lemma is_precategory_mod_precategory_data : is_precategory (mod_precategory_data). Proof. apply is_precategory_one_assoc_to_two. apply make_dirprod. - apply make_dirprod. + intros M N f. use total2_paths_f. * apply funextfun. intro x. apply idpath. * apply isapropismodulefun. + intros M N f. use total2_paths_f. * apply funextfun. intro x. apply idpath. * apply isapropismodulefun. - intros M N P Q f g h. use total2_paths_f. + apply funextfun. intro x. unfold compose. cbn. apply idpath. + 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.