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.
Smaller files allow more fine-grained dependencies, more parallel compilation, and give a more natural structuring when lemmas don't have a natural linear ordering on them, and instead have a natural tree-like ordering.