proposition: Lemma isapropiscomm {X : hSet} (opp : binop X) : isaprop (iscomm opp).
proof: Proof. apply impred. intros x. apply impred. intro x'. simpl. apply (setproperty X). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions