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.
A nicer alternative to using `%nat` here is to use
```coq
Arguments extendable_to_O _ (_ _)%type _ _%nat.
```
where we declare `extendable_to_O`.  (The reason this isn't automatic is that the last argument is hidden by `ooExtendableAlong`.)