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.
Oh, wait, I lied.  It's not an equivalence without funext.  In which case, you're right, the proof is trivial when `n <> 1`.

Now I remember: the reason I stated and proved this as a function, rather than as a "`<~>`" equivalence directly, is that the latter would require funext, whereas I wanted to apply it in a context without funext.  But one could separately prove that if funext holds, then this is an equivalence.