proposition: Lemma iscommmonob {X Y : setwithbinop} (f : binopmono X Y) (is : iscomm (@op Y)) : iscomm (@op X).
proof: Proof. set (axf := pr2 f). simpl in axf. intros a b. apply (invmaponpathsincl _ (pr2 (pr1 f))). rewrite (axf a b). rewrite (axf b a). apply is. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions