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.
This is actually an equivalence, right?  (Though it only matters for `n = 1`, if I understand correctly.)  Do you ever end up needing this fact / is it something we want?