Lemma ismonoidcarrier {X : monoid} (A : submonoid X) : ismonoidop (@op A). Proof. split. - intros a a' a''. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply (assocax X). - exists (make_carrier _ 1 (pr2 (pr2 A))). split. + simpl. intro a. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply (lunax X). + intro a. apply (invmaponpathsincl _ (isinclpr1carrier A)). simpl. apply (runax X). Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.