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.

[martinescardo]

I think these results are still in premature form. You need to think more about this. I am not sure the propositional versions are interesting.

[martinescardo]

Should this really be called System F resizing? Is this the same form of impredicativity as in CoC?

[martinescardo]

In any case, if we agree that this is the same as in System F, it probably should be called System F impredicativity, I think.

[martinescardo]

You already said this in line 97.

[martinescardo]

This is because propositional resizing implies that, which we already know.

[martinescardo]

If you choose A to be a proposition and P to be constantly true, then (Ɐ x ꞉ A , P x) holds is A x 1 which is equivalent to A. Therefore, combining this with the statement in lines 88-89, we get that Propositional-System-F-Resizing is the same thing as propositional resizing.

[ayberkt]

If you choose A to be a proposition and P to be constantly true, then (Ɐ x ꞉ A , P x) holds is A x 1

That would be A ⇒ 𝟙, which is just 𝟙, and not A × 𝟙.

In fact, this would mean that System-F-Resizing implies propositional-resizing, which cannot be the case since the former is validated and the latter is refuted in the cubical assemblies model. I learned this from @slspeight.

So I think Propositional-System-F-Resizing is actually a sensible thing to consider.

[martinescardo]

Again consider A a proposition and B x = 1 to conclude that this is equivalent to propositional resizing.

[ayberkt]

Right, this one is equivalent to propositional resizing.