fact: Definition make_setwith2binop (X : hSet) (opps : (binop X) × (binop X)) : setwith2binop := tpair (λ X : hSet, (binop X) × (binop X)) X opps.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions