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.
Sure.  I think it would still be nicer, for future users, to give the `Arguments` command so they don't have to use `%nat` if they don't want to, even if you do leave `%nat` here.