Definition apsetwith2binop_setwith2binop : apsetwith2binop → setwith2binop := λ X : apsetwith2binop, apSet_pr1 (apsetwith2binop_pr1 X),, pr1 (pr1 (pr2 X)),, pr1 (pr2 (pr2 X)).
Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions.