Take some first steps in investigating System F resizing as an axiom

[ayberkt]

This PR adds a new module in which I summarize various discussions with @slspeight. Here is a short list of things contributed in the module:

• A special case of “System F resizing” that should be consistent.
• The proof that this implies ꪪ-resizing from 𝓤₁ to 𝓤₀.
• A notion of Σ-resizing which immediately gives 𝓤₀ is 𝓤₀ small.
• A notion of ∃-resizing, which is consistent because it is implied by propositional resizing.