Definition carrierofsubmonoid {X : monoid} (A : submonoid X) : monoid. Proof. exists A. apply ismonoidcarrier. Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.