fact: Definition binop2iso {X Y : setwith2binop} (f : twobinopiso X Y) : binopiso (setwithbinop2 X) (setwithbinop2 Y) := @make_binopiso (setwithbinop2 X) (setwithbinop2 Y) (pr1 f) (pr2 (pr2 f)).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions