Extensional concepts in intensional type theory, revisited
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908723647086592 |
|---|---|
| author | Kapulkin, Chris Li, Yufeng |
| author_facet | Kapulkin, Chris Li, Yufeng |
| contents | Revisiting a classic result from M. Hofmann's dissertation, we give a direct proof of Morita equivalence, in the sense of V. Isaev, between extensional type theory and intensional type theory extended by the principles of functional extensionality and of uniqueness of identity proofs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2310_05706 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Extensional concepts in intensional type theory, revisited Kapulkin, Chris Li, Yufeng Logic Logic in Computer Science Category Theory 03B38, 18N45 Revisiting a classic result from M. Hofmann's dissertation, we give a direct proof of Morita equivalence, in the sense of V. Isaev, between extensional type theory and intensional type theory extended by the principles of functional extensionality and of uniqueness of identity proofs. |
| title | Extensional concepts in intensional type theory, revisited |
| topic | Logic Logic in Computer Science Category Theory 03B38, 18N45 |
| url | https://arxiv.org/abs/2310.05706 |