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.
Wording nit: I think "It turns out that for n > 1, being n-path-split is the same as being an equivalence." is clearer; I spent a bit of time trying to figure out if "being n-path-split for n > 1" wanted an implicit "any" or an implicit "all".