Definition monoiddirprod (X Y : monoid) : monoid. Proof. exists (setwithbinopdirprod X Y). apply ismonoiddirprod. Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.