Definition eqrel_on_bool (P:hProp) : eqrel boolset. Proof. set (ifb := bool_rect (λ _:bool, hProp)). exists (λ x y, ifb (ifb htrue P y) (ifb P htrue y) x). repeat split. { intros x y z a b. induction x. - induction z. + exact tt. + induction y. * exact b. * exact a. - induction z. + induction y. * exact a. * exact b. + exact tt. } { intros x. induction x; exact tt. } { intros x y a. induction x; induction y; exact a. } Defined.