Upsetting The New World Order

I refine a dependent type theory with a system of "worlds" that say "where" things are, separately from what they are. Worlds are preordered by "accessibility", with the variable rule ensuring that information flows only in accordance. The variable rule thus represents a promise which we must keep by establishing that “upward" transportation of all constructions is admissible. Types thus need to be portable, which provokes some fresh thinking about how we manage quantification. The payoff is that any upward-closed set of worlds admits a Church-to-Curry-style erasure. I'll discuss a variety of situations which might be modelled by worldly type systems, not least the indexing of algebraic effects.