Lemma isapropissubmodule {R : ring} {M : module R} (A : hsubtype M) : isaprop (issubmodule A). Proof. intros. apply (isofhleveldirprod 1). - apply isapropissubgr. - apply impred. intro x. apply impred. intro m. apply impred. intro a. apply (pr2 (A _)). Defined.
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.