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.
Yes, that, and so that no one outside this file will end up using this version accidentally (e.g. because they forgot to import `Localization`).  I'll clarify the comment.