mathlib

a7e80393 - feat(data/equiv/encodable): `ulower` lowers countable types to `Type 0` (#2574)

feat(data/equiv/encodable): `ulower` lowers countable types to `Type 0` (#2574) Given a type `α : Type u`, we can lift it into a higher universe using `ulift α : Type (max u v)`. This PR introduces an analogous construction going in the other direction. Given an encodable (= countable) type `α : Type u`, we can lower it to the very bottom using `ulower α : Type 0`. The equivalence is primitive recursive if the type is primcodable. The definition of the equivalence was already present as `encodable.equiv_range_encode`. However it is very inconvenient to use since it requires decidability instances (`encodable.decidable_range_encode`) that are not enabled by default because they would introduce overlapping instances that are not definitionally equal.