refactor(data/equiv): split out `./set` from `./basic` (#9560)
This move all the equivalences between sets-coerced-to-types to a new file, which makes `equiv/basic` a slightly more manageable size.
The only non-move change in this PR is the rewriting of `equiv.of_bijective` to not go via `equiv.of_injective`, as we already have all the fields available directly and this allows the latter to move to a separate file.
This will allow us to import `order_dual.lean` earlier, as we no longer have to define boolean algebras before equivalences are available.
This relates to #4758.
