fact: Definition twobinopincltotwobinopfun (X Y : setwith2binop) : twobinopmono X Y -> twobinopfun X Y := λ f, make_twobinopfun (pr1 (pr1 f)) (pr2 f).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions