Dialectica models of type theory

DOI10.1145/3209108.3209207MaRDI QIDQ5145350zbMATH OpenOpenAlexFDO

Authors Sean Moss, Tamara von Glehn

Publication date 20 January 2021

Published in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2105.00283, https://ora.ox.ac.uk/objects/uuid:36d42f84-22c0-4db1-b991-92b6d96fcc02

Mathematics Subject Classification ID

Type theory (03B38)

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.

Recommendations

• Intensional models for the theory of types
• Abstract deduction and inferential models for type theory
• A modular construction of type theories
• Homotopy-theoretic models of type theory
• scientific article; zbMATH DE number 5872253
• scientific article; zbMATH DE number 1497733
• scientific article; zbMATH DE number 1302061
• Representing model theory in a type-theoretical logical framework
• Representing model theory in a type-theoretical logical framework
• Analogical type theory

Cited in

(14)

• Dialectica logical principles
• Dialectica principles via Gödel doctrines
• The Dialectica monad and its cousins
• scientific article; zbMATH DE number 4104952 (Why is no real title available?)
• Identity types and weak factorization systems in Cauchy complete categories
• Dialectica categories and games with bidding
• CHAD for expressive total languages
• Monoidal closure of Grothendieck constructions via -tractable monoidal structures and Dialectica formulas
• Weihrauch problems as containers
• Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
• is for Dialectica
• A 2-categorical approach to the semantics of dependent type theory with computation axioms
• Free doubly-infinitary distributive categories are Cartesian closed
• Cartesian closed Dialectica categories

This page was built for publication: Dialectica models of type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145350)