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