fact: Definition make_subsetswith2binop {X : setwith2binop} : ∏ (t : hsubtype X), (λ A : hsubtype X, issubsetwith2binop A) t → ∑ A : hsubtype X, issubsetwith2binop A := tpair (λ A : hsubtype X, issubsetwith2binop A).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions