fact: Definition make_twobinophrel {X : setwith2binop} : ∏ (t : hrel X), (λ R : hrel X, is2binophrel R) t → ∑ R : hrel X, is2binophrel R := tpair (λ R : hrel X, is2binophrel R).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions