Definition ismonoidfunisbinopfun {X Y : monoid} {f : X → Y} (H : ismonoidfun f) : isbinopfun f := dirprod_pr1 H.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.