fact: Definition make_istwobinopfun {X Y : setwith2binop} (f : X -> Y) (H1 : ∏ x x' : X, paths (f (op1 x x')) (op1 (f x) (f x'))) (H2 : ∏ x x' : X, paths (f (op2 x x')) (op2 (f x) (f x'))) : istwobinopfun f := make_dirprod H1 H2.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions