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.
Which part of the following proof needs funext?
- `ishprop_extendable`
- `symmetry` of equivalences
- `ExtendableAlong n f C <-> ExtendableAlong n f D`
- `equiv_iff_hprop`