Lemma isapropissubmonoid {X : monoid} (A : hsubtype X) : isaprop (issubmonoid A). Proof. apply (isofhleveldirprod 1). - apply isapropissubsetwithbinop. - apply (pr2 (A 1)). Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.