proposition: Lemma eqrel_on_bool_iff (P:hProp) (E := eqrel_on_bool P) (f := setquotpr E) : f true = f false <-> P.
proof: 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.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Sets