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