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.
It is (presumably) an equivalence, and in principle that might matter for any `n` because it's true even without funext.  But I never ended up needing that, so I was lazy.