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.
;Note: If you want these blocks of code to display nicely in coqdoc, you should set them off with `<<` and `>>` as in:
```coq
<<
code block here
>>
```