fact: Definition ismonoidopisof {X Y : setwithbinop} (f : binopiso X Y) (is : ismonoidop (@op X)) : ismonoidop (@op Y) := make_dirprod (isassocisof f (pr1 is)) (isunitalisof f (pr2 is)).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions