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.
Perhaps it's worth doing that, then?

At some point, I (or someone else) should make a pass over all of the `IsEquiv` instances, and be systematic about which ones to allow and give them systematic priorities.  I'm generally pretty happy with the `IsTrunc` inference on the simple cases, and I feel like this is a sufficiently simple case of `IsEquiv` that we should be able to handle it ~instantaneously.