Polyadic Quantifiers on Dependent Types

An interaction between dependency relations and quantification underlies numerous phenomena in natural language. Dependencies are responsible for inverting scope, as illustrated by the example a day of every month. The part-whole relation, expressed by the preposition of in this example, introduces a dependency between wholes (months) and their respective parts (days). Quantifying over this dependency yields the inverse scope reading: for every month, there is a different day that belongs to it. Dependencies are also needed for tracking anaphoric reference to quantifier domains, as illustrated by the sentence Every farmer who owns a donkey beats it. By quantifying universally over the dependency between each of the farmers and the donkeys owned by them, we obtain the intended reading that every farmer beats every donkey he owns. In this paper, we show that polyadic quantifiers on dependent types are well-suited for modelling the interaction of dependency relations and quantification in these phenomena. Then we present, in a conceptual way, the mathematics behind the process of polyadic quantification over dependent types. The main new feature is the left strength on the cartesian monad over a basic fibration of a topos. It combines with what we call the right strength into an operation (pile’up) that turns tuples of quantifiers into polyadic ones.