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