proposition: Lemma is_precategory_mod_precategory_data : is_precategory (mod_precategory_data).
proof: 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.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.Algebra.Modules UniMath.Algebra.Modules.Examples UniMath.CategoryTheory.Limits.Zero