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.
Nit: Does this solve 1 completely?  If so, you should probably use `exact`, because, in general, I think `apply idmap` works but is a no-op.