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.
Note: If you do `assert` rather than `pose`, or you do `pose proof (body) as name`, you won't have to `clearbody`.