fact: Definition apsetwith2binop_setwith2binop : apsetwith2binop -> setwith2binop := λ X : apsetwith2binop, apSet_pr1 (apsetwith2binop_pr1 X),, pr1 (pr1 (pr2 X)),, pr1 (pr2 (pr2 X)).
imports: UniMath.Algebra.BinaryOperations UniMath.Foundations.Propositions UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions