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.
I think probably not, though I'm not sure, and tend to be a bit careless.  You can see [pseduofunctrors](https://github.com/HoTT/HoTT/blob/master/theories/categories/Pseudofunctor/Core.v) for [an example](http://hott.github.io/HoTT/coqdoc-html/HoTT.categories.Pseudofunctor.Core.html#) of what it looks like when you do indent (it's not terrible).