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, for some meaning of "planning".  (-: It's not very high up on the to-do list.  I haven't sat down to figure out the best way to state propositional resizing either, but it'd be something like `IsEquiv (lift : hProp -> hProp)`.  We'd want it to be a polymorphic axiom, maybe controlled by a dummy typeclass like funext and univalence.  It might also be better to state it in a form that makes sense without univalence, I'm not sure.