Definition submoduleadd (x y : M) : A x -> A y -> A (x + y). Proof. intros ax ay. exact (pr1 (pr1 (pr1 (pr2 A))) (make_carrier A x ax) (make_carrier A y ay)). 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.