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.
This is a bit confusing.  You have `Funext` available in the section, and yet you claim that `Op'` doesn't depend on `Funext`.  If this is truely the case, why not just make `Funext` an argument to `accessible_op` (and pay the minor cost of having to specify `U` separately for each one)?