mathlib

7ce47174 - refactor(computability/reduce): define many-one degrees without parameter (#2630)

refactor(computability/reduce): define many-one degrees without parameter (#2630) The file `reduce.lean` defines many-one degrees for computable reductions. At the moment every primcodable type `α` has a separate type of degrees `many_one_degree α`. This is completely antithetical to the notion of degrees, which are introduced to classify problems up to many-one equivalence. This PR defines a single `many_one_degree` type that lives in `Type 0`. We use the `ulower` infrastructure from #2574 which shows that every type is computably equivalent to a subset of natural numbers. The function `many_one_degree.of` which assigns to every set of a primcodable type a degree is still universe polymorphic. In particular, we show that `of p = of q ↔ many_one_equiv p q`, etc. in maximal generality, where `p` and `q` are subsets of different types in different universes. See previous discussion at #1203.