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 it belongs in `Extensions`.  I could see putting it in `DependentExtensions`, I guess, although I doubt that it has any application outside of localizations.  But maybe you would argue that even if it has no other use, separating it out would have other benefits?