Lemma intersection_submodule {R : ring} {M : module R} {I : UU} (S : I -> hsubtype M) (each_is_submodule : ∏ i : I, issubmodule (S i)) : issubmodule (subtype_intersection S). Proof. intros. use make_issubmodule. - exact (intersection_subgr S (λ i, (pr1 (each_is_submodule i)))). - intros r m a i. exact (pr2 (each_is_submodule i) r m (a i)). Qed.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Modules.Core.