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 takes about .6 seconds to solve the goal `IsEquiv (equiv_extendable_pathsplit n.+2 C f)` with `apply @equiv_isequiv` and another .6 seconds to solve the goal `IsEquiv (equiv_extendable_pathsplit n.+2 C f)^-1` with `(*external*) apply @isequiv_inverse`.  This accounts for the entire 1.2 seconds of the refine on my machine.  You can cut this time in half by refreshing the hint database with `Hint Extern 0 (IsEquiv (equiv_fun _)) => apply @equiv_isequiv : typeclass_instances.`  I haven't figured out how to solve the `equiv_inv` goal quickly.