Add properties of `∃!` (and refactor it?)

[gallais]

We define ∃! but we have literally zero properties about it. Some ideas:

properties:

• ∃! P implies ∃! Q given that P <=> Q

refactor:

• ∃! defined over a Setoid rather than a set + a binary relation?
• Add Unique x P = ∀ {y} → B y → x ≈ y to Relation.Unary? (and prove its properties & use that when proving that of ∃!)

[HuStmpHrrr]

I think defining over setoids seems more consistent.

As P Q : A -> Set b, to state P <=> Q seems to require extentionality already, does it not? Then why not just work with setoids?

[gallais]

P <=> Q was hand-wavy; I meant P ⊆ Q and Q ⊆ P (with this _⊆_).
Or equivalently ∀ {x} → P x ⇔ Q x (with this _⇔_).

It may be worth explicitly introducing such an equivalence combinator for Predicate in Relation.Unary.

[jamesmckinna]

P for B in item 2 of @gallais 's original 'refactor' proposal.
What is/are the consequence(s) of issue #759 / PR #793 , in general, for this issue?