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