## 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: | 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. |

Pages: | 10 |

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

Paper: |