2018/06/27 by Sean Moss, Sean K. Moss, Tamara von Glehn
Computer Science · Mathematics · #Algebra over a field #Categorical variable #Category theory #Computer science #Construct (python library) #Functor #Homotopy and Cohomology in Algebraic Topology #Interpretation (philosophy) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematics #Monad (category theory) #Programming language #Pure mathematics #Set (abstract data type) #Set theory #Type (biology) #Type theory #Universal algebra #cs.LO #math.CT
paper · pdf · doi:10.1145/3209108.3209207
published as LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science July 2018
openalex publication_date 2018/06/27 · arxiv created 2021/05/01 · arxiv updated 2021/05/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
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.