Lemma setquotbooleqintcomp {X : UU} (R : eqrel X) (is : ∏ x x' : X, isdecprop (R x x')) : iscomprelfun2 R (setquotbooleqint R is). Proof. intros. unfold iscomprelfun2. intros x x' x0 x0' r r0. unfold setquotbooleqint. induction (pr1 (is x x0)) as [ r1 | nr1 ]. - induction (pr1 (is x' x0')) as [ r1' | nr1' ]. + apply idpath. + induction (nr1' (eqreltrans R _ _ _ (eqreltrans R _ _ _ (eqrelsymm R _ _ r) r1) r0)). - induction (pr1 (is x' x0')) as [ r1' | nr1' ]. + induction (nr1 (eqreltrans R _ _ _ r (eqreltrans R _ _ _ r1' (eqrelsymm R _ _ r0)))). + apply idpath. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.