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.
Ah, by "hypothesis" I meant something in the context of a proof (introduced with `pose`), not a section-local-variable.  And I can't make `ooExtendableAlong` a notation since then I can't annotate it with universes as in the definition of `ReflectiveSubuniverse`.  (Well, actually, the annotation is accepted, but apparently silently ignored.)  But I can `Local Open Scope nat_scope` to make it override the notation `1` for `idpath` in `path_scope`.  (I'm starting to wonder whether it's really worth having `1` as a notation for `idpath`.)