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