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.
Right, thanks.  But I could only do that for `hs`, since I need the body of `h` to define `hs`, so I think I find it easier to read this way.