Different scope-taking mechanisms have been proposed for capturing quantifier-scope alternation, including covert operations of quantifier movement (e.g. May 1978, 1985), type-changing rules (Hendriks 1993), storage devices (Cooper 1983). In my talk, I will present a new scope-taking system with dependent types (Martin-Löf 1975, 1984, Makkai, 1995). The key features are: (i) richly typed system; (ii) contexts for determining the relative scoping of quantifiers; (iii) recursive procedure by which the interpretation is computed and the dependently typed context is built along the surface structure tree. The main advantage of our proposal is that it does not overgenerate --- it produces all and only the attested readings. The core idea behind the proposal is that certain lexical elements (interpreted as dependent types) are responsible for inverting scope: relational nouns and locative prepositions. This allows us to provide a principled solution to the puzzle of why certain constructions missing such elements block inverse scope. This is joint work with Marek Zawadowski.