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.
Nice, thanks.  What about the other occurrences of `%nat`, in `O_inverts_generators`, `ooextendable_isnull_fibers`, and `accessible_cl`?  In all those cases the argument is being passed to a local hypothesis rather than a global function; would I have to say `Arguments` on the hypothesis?  Can I even do that?

Even better, is there any way to make `ooExtendableAlong` "transparent" to scope binding?