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.
> Is there a reason you don't let the X in IsNull depend on i and then use IsNull (hfiber f) C?

Because mathematically, that's not what "null" means.

By the way, I decided that this lemma really belongs in `Extensions.v`, so this line of the diff is about to be out of date.