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`?