Definition setquotbooleq {X : UU} (R : eqrel X) (is : ∏ x x' : X, isdecprop (R x x')) : setquot R -> setquot R -> bool := setquotuniv2 R (make_hSet _ (isasetbool)) (setquotbooleqint R is) (setquotbooleqintcomp R is).
Require Import UniMath.Foundations.UnivalenceAxiom.