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