Dialectica models of type theory
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...
| Main Authors: | , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Association for Computing Machinery
2018
|
| _version_ | 1797062659320840192 |
|---|---|
| author | Moss, SK von Glehn, T |
| author_facet | Moss, SK von Glehn, T |
| author_sort | Moss, SK |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T20:48:42Z |
| format | Conference item |
| id | oxford-uuid:36d42f84-22c0-4db1-b991-92b6d96fcc02 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T20:48:42Z |
| publishDate | 2018 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:36d42f84-22c0-4db1-b991-92b6d96fcc022022-03-26T13:40:20ZDialectica models of type theoryConference itemhttp://purl.org/coar/resource_type/c_5794uuid:36d42f84-22c0-4db1-b991-92b6d96fcc02EnglishSymplectic ElementsAssociation for Computing Machinery2018Moss, SKvon Glehn, TWe 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. |
| spellingShingle | Moss, SK von Glehn, T Dialectica models of type theory |
| title | Dialectica models of type theory |
| title_full | Dialectica models of type theory |
| title_fullStr | Dialectica models of type theory |
| title_full_unstemmed | Dialectica models of type theory |
| title_short | Dialectica models of type theory |
| title_sort | dialectica models of type theory |
| work_keys_str_mv | AT mosssk dialecticamodelsoftypetheory AT vonglehnt dialecticamodelsoftypetheory |