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, I'll change it.

If you could figure out how to make `IsEquiv` inference faster, that would be nice.  I've noticed elsewhere that Coq is sometimes quite slow to pick up `equiv_isequiv` and `isequiv_inverse`, which seems inexcusable.  Maybe those instance should have lower priority than everything else?