Lemma eqrel_on_bool_iff (P:hProp) (E := eqrel_on_bool P) (f := setquotpr E) : f true = f false <-> P. Proof. split. { intro q. change (E true false). apply (invmap (weqpathsinsetquot _ _ _)). change (f true = f false). exact q. } { intro p. apply iscompsetquotpr. exact p. } Defined.