fact: Definition twobinopisototwobinopmono (X Y : setwith2binop) : twobinopiso X Y -> twobinopmono X Y := λ f, make_twobinopmono (weqtoincl (pr1 f)) (pr2 f).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions