fact: Definition isabmonoidopisob {X Y : setwithbinop} (f : binopiso X Y) (is : isabmonoidop (@op Y)) : isabmonoidop (@op X) := tpair _ (ismonoidopisob f is) (iscommisob f (commax_is is)).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions