Definition quotdecrelint {X : UU} {R : hrel X} (L : decrel X) (is : iscomprelrel R (pr1 L)) : brel (setquot R). Proof. intros. set (f := decreltobrel L). unfold brel. apply (setquotuniv2 R boolset f). intros x x' x0 x0' r r0. unfold f. unfold decreltobrel in *. induction (pr2 L x x0') as [ l | nl ]. - induction (pr2 L x' x0') as [ l' | nl' ]. + induction (pr2 L x x0) as [ l'' | nl'' ]. * apply idpath. * set (e := is x x' x0 x0' r r0). induction e. induction (nl'' l'). + induction (pr2 L x x0) as [ l'' | nl'' ]. * set (e := is x x' x0 x0' r r0). induction e. induction (nl' l''). * apply idpath. - induction (pr2 L x x0) as [ l' | nl' ]. + induction (pr2 L x' x0') as [ l'' | nl'' ]. * apply idpath. * set (e := is x x' x0 x0' r r0). induction e. induction (nl'' l'). + induction (pr2 L x' x0') as [ l'' | nl'' ]. * set (e := is x x' x0 x0' r r0). induction e. induction (nl' l''). * apply idpath. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.