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.
Yeah, I don't proof-local variables get argument scopes:
```coq
Definition foo (n : nat) := n.                                                                |
Goal True.
  pose foo as bar.
  pose (foo 1).
  pose (bar 1). (* failure *)
```