Definition issubring {X : ring} (A : hsubtype X) : UU := (@issubgr X A) × (@issubmonoid (ringmultmonoid X) A).
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.