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.
```coq
Section foo.
  Definition x := Type -> nat -> Type.
  Variable y : x.
  Arguments y _%type_scope _%nat_scope.
  Check y (Set * Set) (1 * 1).
```
works.  Alternatively, you can make `ooExtendableAlong` an alias/notation.

I've made [bug 3793](https://coq.inria.fr/bugs/show_bug.cgi?id=3793) asking for a feature to declare constants appropriately transparent, or to autonormalize them appropriately if it's not too expensive.