Dialectica models of type theory

Authors: Sean Moss and Tamara von Glehn

Paper Information

Title:Dialectica models of type theory
Authors:Sean Moss and Tamara von Glehn
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:category theory, dependent type theory, Martin-Löf type theory, display map category, logical predicates, gluing, functional interpretation, Dialectica interpretation, polynomial functor, Diller-Nahm variant, additive monad, dependent product types, finite sum types, extensive category

ABSTRACT. We present two Dialectica-like constructions for models of intensional Martin-Löf type theory based on Gödel's original Dialectica interpretation and the Diller-Nahm variant, bringing dependent types to categorical proof theory. We set both constructions within a logical predicates style theory for display map categories where we show that 'quasifibred' versions of dependent products and universes suffice to construct their standard counterparts. To support the logic required for dependent products in the first construction, we propose a new semantic notion of finite sum for dependent types, generalizing finitely-complete extensive categories. The second avoids extensivity assumptions using biproducts in a Kleisli category for a fibred additive monad.

Talk:Jul 11 11:00 (Session 64E)