Dialectica models of type theory

TL;DR

This paper introduces two Dialectica-like models for intensional Martin-Löf type theory, utilizing categorical proof theory techniques and new semantic notions to handle dependent types and universes.

Contribution

It develops two novel categorical constructions for models of dependent type theory based on Dialectica interpretations, extending the proof-theoretic framework to dependent types.

Findings

Both models incorporate dependent types within categorical proof theory.

A new semantic notion of finite sum for dependent types is proposed.

The second model uses biproducts in a fibred additive monad to avoid extensivity assumptions.

Abstract

We present two Dialectica-like constructions for models of intensional Martin-L\"of type theory based on G\"odel'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.