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.
I don't think so.  Say we have `IsEquiv (lift : hProp@{Set} -> hProp@{super_lg})`, for some fixed but arbitrary `super_lg`, and we want to resize an `hProp@{lg}` down to an `hProp@{sm}` where `Set <= sm <= lg < super_lg`.  We can lift `hProp@{lg} -> hProp@{super_lg}` without any axioms.  We can use our resizing hypothesis to turn this into an `hProp@{Set}`.  We can lift `hProp@{Set}` to `hProp@{sm}` without any axioms.  Moreover, this should provably be an inverse to `lift : hProp@{sm} -> hProp@{lg}`.