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 don't understand; the resizing axiom should be a statement about all
universes, not just all universes smaller than some fixed bound.
On Nov 9, 2014 2:11 AM, "Jason Gross" <notifications@github.com> wrote:

> In theories/Modality.v:
>
> >  (** ** Examples *)
> >
> > -(** Finally, we give one nontrivial example of a modality.  This is Exercise 7.12 in the book. *)
> > -Definition notnot_modality `{Funext} : Modality.
> > +(** Finally, we give one nontrivial example of a modality.  This is Exercise 7.12 in the book.  Note that it is (apparently) *not* accessible unless we assume propositional resizing. *)
>
> Oops, missed this. As long as you don't try to resize your resizing axiom,
> and you don't need to stick your resizing axiom itself inside of something,
> then you can let super_lg be as large as you like. Is there anything that
> the resizing axiom itself needs to go inside of?
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/603/files#r20057848>.
>