fact: Definition binop2mono {X Y : setwith2binop} (f : twobinopmono X Y) : binopmono (setwithbinop2 X) (setwithbinop2 Y) := @make_binopmono (setwithbinop2 X) (setwithbinop2 Y) (pr1 f) (pr2 (pr2 f)).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions