Make primitives in the prelude universe-polymorphic

[flupe]

Using those can prove to be annoying on the Agda side:

https://github.com/agda/agda2hs/blob/15314cd3fbc505ead13e48257194afd5ca171672/lib/Haskell/Prim.agda#L38

We may want to make it dependent too, so long as we annotate with erasure properly.