chore(data/equiv/basic): add many docstrings, review (#3008)
Non-docstring changes:
* drop `decidable_eq_of_equiv` (was a copy of `equiv.decidable_eq`);
* rename `inhabited_of_equiv` to `equiv.inhabited`;
* rename `unique_of_equiv` to `equiv.unique`, take `unique β` as an
instance argument;
* better defeq for `equiv.list_equiv_of_equiv`;
* use `coe` instead of `subtype.val` in `equiv.set.union'`;
* use `s ∩ t ⊆ ∅` instead of `s ∩ t = ∅` in `equiv.set.union`;
this way it agrees with `disjoint`;
* use `[decidable_pred (λ x, x ∈ s)]` instead of `[decidable_pred s]`
in `equiv.set.union`;
* use `coe` instead of `subtype.val` in `equiv.set.sep`;
* make `f` an explicit argument in `equiv.of_bijective f hf`;
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
