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.
You might be able to fix the problem in `O_inverts_generators` with `pose (ext_dom := ... : _ -> nat -> _).`  (where the `_`s are literal `_`s, and the `...` is meant to be given in the source with the body you currently have).