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.
Doesn't the "use resizing to get it down to an arbitrarily small type" require the resizing axiom to be polymorphic, so it can be applied at whatever sufficiently high level you lifted it up to?