一句话：基于 Gödel 的 Dialectica 解释及其 Diller–Nahm 变体，为内涵 Martin-Löf 类型论构造两种范畴模型。
本文把 Gödel 的 Dialectica 解释与 Diller–Nahm 变体推广到依赖类型论，为内涵 Martin-Löf 类型论给出两种 Dialectica 式范畴模型，从而将依赖类型引入范畴证明论。作者在 display map 范畴的逻辑谓词风格理论中开展构造，证明依赖积与 universe 的“quasifibred”版本足以构造其标准对应物。为支持第一种构造中依赖积所需的逻辑，作者提出依赖类型的一种新语义概念——有限和，推广了有限完备可扩张范畴。第二种构造则利用 fibred additive monad 的 Kleisli 范畴中的双积，避免了对可扩张性的假设。
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.