Lemma isaset_submonoid (A : monoid) : isaset (submonoid A). Proof. apply isaset_total2. - apply isasethsubtype. - intro P. apply isasetaprop, isapropissubmonoid. Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.