Move ObjectClassifier and UniverseLevel out of types/

The files in `types/` follow a fairly standard structure, proving computational facts about a particular type former.  `ObjectClassifier` and `UniverseLevel` don't fit.

Also, delete `contrib/V.v` since we now have `hit/V.v`.