fact: Definition is2binophrel {X : setwith2binop} (R : hrel X) : UU := dirprod (@isbinophrel (setwithbinop1 X) R) (@isbinophrel (setwithbinop2 X) R).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions