fact: Definition issubsetwith2binop {X : setwith2binop} (A : hsubtype X) : UU := dirprod (∏ a a' : A, A (op1 (pr1 a) (pr1 a'))) (∏ a a' : A, A (op2 (pr1 a) (pr1 a'))).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions