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.
To be clear: `<<` and `>>` should not be indented, I'm pretty sure.  I'm unsure whether the code inside should be indented.