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