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