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's not immediately clear which is the "other" version in this comment.  I'd use `We call the [Nul (fun (_:Unit) => U] version [Op']` if that's what you mean (or `We call the non-[Funext] version [Op']` or `We call the non-HIT version [Op']` or whatever).