Unifying cubical and multimodal type theory
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2022
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913614856716288 |
|---|---|
| author | Aagaard, Frederik Lerbjerg Kristensen, Magnus Baunsgaard Gratzer, Daniel Birkedal, Lars |
| author_facet | Aagaard, Frederik Lerbjerg Kristensen, Magnus Baunsgaard Gratzer, Daniel Birkedal, Lars |
| contents | In this paper we combine the principled approach to modalities from multimodal type theory (MTT) with the computationally well-behaved realization of identity types from cubical type theory (CTT). The result -- cubical modal type theory (Cubical MTT) -- has the desirable features of both systems. In fact, the whole is more than the sum of its parts: Cubical MTT validates desirable extensionality principles for modalities that MTT only supported through ad hoc means. We investigate the semantics of Cubical MTT and provide an axiomatic approach to producing models of Cubical MTT based on the internal language of topoi and use it to construct presheaf models. Finally, we demonstrate the practicality and utility of this axiomatic approach to models by constructing a model of (cubical) guarded recursion in a cubical version of the topos of trees. We then use this model to justify an axiomatization of Löb induction and thereby use Cubical MTT to smoothly reason about guarded recursion. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2203_13000 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Unifying cubical and multimodal type theory Aagaard, Frederik Lerbjerg Kristensen, Magnus Baunsgaard Gratzer, Daniel Birkedal, Lars Logic in Computer Science In this paper we combine the principled approach to modalities from multimodal type theory (MTT) with the computationally well-behaved realization of identity types from cubical type theory (CTT). The result -- cubical modal type theory (Cubical MTT) -- has the desirable features of both systems. In fact, the whole is more than the sum of its parts: Cubical MTT validates desirable extensionality principles for modalities that MTT only supported through ad hoc means. We investigate the semantics of Cubical MTT and provide an axiomatic approach to producing models of Cubical MTT based on the internal language of topoi and use it to construct presheaf models. Finally, we demonstrate the practicality and utility of this axiomatic approach to models by constructing a model of (cubical) guarded recursion in a cubical version of the topos of trees. We then use this model to justify an axiomatization of Löb induction and thereby use Cubical MTT to smoothly reason about guarded recursion. |
| title | Unifying cubical and multimodal type theory |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2203.13000 |