David Corfield type-shifting

Barbara Partee, Noun Phrase Interpretation and Type-shifting principles.

Does it all take place in Montague semantics?

Their lifting seems to be the continuation monad?.

Their ‘ident’ is the passage $a: A$ shift to $x: A \vdash Id(x, a): Type$ or $Id(-,a): A \to Type$.