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.
Use `forall _ (_ : nat), _` instead of `_ -> nat -> _`, I think.  (`_UNBOUND_REL_n` is almost always an indicator that you're using a non-dependent function where you need a dependent one.)