HoTT/HoTT — pull request #480 by mikeshulman (2014-09-09 15:27:49+00:00)
Title: 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`.