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.
Well, you get it automatically for `n <> 1`, because you proved above that it's an hProp.  (Perhaps I should have said, "though the proof is only non-trivial for `n = 1`.)