Definition totalsubmonoid (X : monoid) : submonoid X. Proof. exists (totalsubtype X). split. - intros x x'. apply tt. - apply tt. Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.