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