Mathlib.Data.Countable.Small
source
That is, any countable type is equivalent to a type in any universe.