proposition: Lemma isapropismonoidop {X : hSet} (opp : binop X) : isaprop (ismonoidop opp).
proof: Proof. apply (isofhleveldirprod 1). apply isapropisassoc. apply isapropisunital. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions