Commit 2021-01-13 18:52 7ce47174

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.