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, apparently the solution is to use `forall i (n : nat), _` (apparently unnamed arguments are treated as non-dependent; I'm not sure if this was always the case).