Definition issubrig {X : rig} (A : hsubtype X) : UU := (@issubmonoid (rigaddabmonoid X) A) × (@issubmonoid (rigmultmonoid X) A).
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.