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

Draft

ayberkt wants to merge 24 commits intomasterfrom system-f-resizing

+356

Commits on May 15, 2024

Add a new module to study System F resizing
ayberkt
committed

Commits on May 21, 2024

Clean up

slspeight
authored and
ayberkt
committed
Write some stuff

slspeight
authored and
ayberkt
committed
Clean up

slspeight
authored and
ayberkt
committed
Add Σ-resizing and ∃-resizing

slspeight
authored and
ayberkt
committed
Add the generalized form of System F resizing

slspeight
authored and
ayberkt
committed
Write some more stuff

slspeight
authored and
ayberkt
committed
Make some progress

slspeight
authored and
ayberkt
committed
Complete the proof from today's meeting

slspeight
authored and
ayberkt
committed
Clean up

slspeight
authored and
ayberkt
committed
Continue to clean up

slspeight
authored and
ayberkt
committed
Clean up

slspeight
authored and
ayberkt
committed
Clean up

slspeight
authored and
ayberkt
committed
Add @slspeight as a contributor

slspeight
authored and
ayberkt
committed
Write down the fact that Σ-resizing gives that 𝓤₀ is 𝓤₀-small

slspeight
authored and
ayberkt
committed
Continue to update comments

slspeight
authored and
ayberkt
committed
Add trivial implication

slspeight
authored and
ayberkt
committed

Commits on May 22, 2024

Commits on May 23, 2024

Commits on May 24, 2024