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.
`refine (trunc_equiv' _ (equiv_inverse (equiv_extendable_pathsplit n.+2 C f)))` is instantaneous, presumably because it never breaks out into typeclass inference at all.