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.
I'm not sure if I'll get a chance to make a thorough pass anytime soon, but here's my idea:
- any rules that decrease the size of the term structurally should get very low priority.  This includes `equiv_isequiv`, `isequiv_inverse`, `IsEquiv f -> IsEquiv g -> IsEquiv (f o g)`, `IsEquiv f -> IsEquiv (ap f)`, etc.
- next higher priority can be things that drop you into other typeclasses, such as `Contr A -> Contr B -> @IsEquiv A B f`
- things that increase the structural complexity of the function should generally not be instances, though it's probably all-right to make them `Hint Immediate` instances