Commit 2020-05-07 22:43 a7e80393

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.