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've modified `Extensions.v` to put the funext hypotheses in explicitly where they are needed and leave them out where they aren't, rather than assuming it everywhere in a section variable.