Lemma iscommdirprod (X Y : abmonoid) : iscomm (@op (setwithbinopdirprod X Y)). Proof. intros xy xy'. induction xy as [ x y ]. induction xy' as [ x' y' ]. simpl. apply pathsdirprod. - apply (commax X). - apply (commax Y). Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.