Definition setquotbooleqint {X : UU} (R : eqrel X) (is : ∏ x x' : X, isdecprop (R x x')) (x x' : X) : bool. Proof. intros. induction (pr1 (is x x')). apply true. apply false. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.