Lemma isassocdirprod (X Y : monoid) : isassoc (@op (setwithbinopdirprod X Y)). Proof. simpl. intros xy xy' xy''. simpl. apply pathsdirprod. - apply (assocax X). - apply (assocax Y). Qed.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.