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.
Oops, missed this.  As long as you don't try to resize your resizing axiom, and you don't need to stick your resizing axiom itself inside of something, then you can let `super_lg` be as large as you like.  Is there anything that the resizing axiom itself needs to go inside of?