Dialectica Categories and Games with Bidding

This paper presents a construction which transforms categorical models of additive-free propositional linear logic, closely based on de Paiva\u27s dialectica categories and Oliva\u27s functional interpretations of classical linear logic. The construction is defined using dependent type theory, which proves to be a useful tool for reasoning about dialectica categories. Abstractly, we have a closure operator on the class of models: it preserves soundness and completeness and has a monad-like structure. When applied to categories of games we obtain \u27games with bidding\u27, which are hybrids of dialectica and game models, and we prove completeness theorems for two specific such models