Commit 2020-06-10 12:49 b427ebf9

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;