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.
There are insane solutions, such as making `1` a notation for a typeclass that can be either a `nat` or a path...

But, yes, for things you `pose`, there's probably not really a better way than adjusting the overall scope stack, or using `%nat`.  (I still think that, in the line this particular comment thread is on, you should use `Arguments` and drop the `%nat`.  It's just not a fully general solution.)