proposition: Lemma isunitindirprod (X Y : monoid) : isunit (@op (setwithbinopdirprod X Y)) (make_dirprod (unel X) (unel Y)).
proof: Proof. split. - intro xy. destruct xy as [ x y ]. simpl. apply pathsdirprod. apply (lunax X). apply (lunax Y). - intro xy. destruct xy as [ x y ]. simpl. apply pathsdirprod. apply (runax X). apply (runax Y). Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders