Universal properties without funext, and localization

See <http://homotopytypetheory.org/2014/11/02/universal-properties-without-function-extensionality/> for a detailed description of the contents of this PR.
Why would we want it to be polymorphic?  (For performance, so that we're not carrying around too many universes?)  Or so that we don't have to explicitly lift and lower `hProp`s?  (In theory, we should only ever need it at one level, right?  We can simply lift any `hProp` up to a sufficiently high level (by destructuring it and using the fact that `lift` is an equivalence), and then use resizing to get it down to an arbitrarily small type, and then re-lift that type to be what we want it to be.  (Another option would be to ask for a proof of `IsEquiv (lift@{i j} : hProp -> hProp)`, but use a polymorphic proof of `IsEquiv (lift'@{x y} : hProp -> hProp)` the precomposes and post-composes with `lift'` to get out a more universe polymorphic version.