The dialectica monad and its cousins
PIETER J. W. HOFSTRA · CRM proceedings & lecture notes · 2011
I give an expositional account of the dialectica construction and some related constructions from the point of view of quantification in fibrations. This allows for concise conceptual formulations of these constructions and explains their universal properties. There are two main points I wish to convey; the first is that the categorical dialectica construction decomposes into two steps, following the quantifier pattern of the original translation; the second is that the categorical embodiment of Skolemization takes the form of a pseudo-distributive law between the pseudo-monads which freely add universal and existential quantification.