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 curious, are you planning on proving that notnot is accessible under a propositional resizing hypothesis?  Would the resizing assumption be something like ``(propositional_resizing : hProp -> hProp) `{IsEquiv propositional_resizing}``?