Lemma isdecquotrel {X : UU} {R : eqrel X} {L : hrel X} (is : iscomprelrel R L) (isl : isdecrel L) : isdecrel (quotrel is). Proof. intros. apply (isdecrellogeqf (quotdecrelintlogeq (make_decrel isl) is) (pr2 (breltodecrel (quotdecrelint (make_decrel isl) is)))). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.