A Cubical Language for Bishop Sets
We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets \`a la Coquand, in which every type enjoys a definitional version of the uniqueness of identity proofs. Using cubical notions, XTT reconstructs many of the ideas underlying Observational Type Theory, a version of...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2022-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/9069/pdf |
| _version_ | 1797268513941880832 |
|---|---|
| author | Jonathan Sterling Carlo Angiuli Daniel Gratzer |
| author_facet | Jonathan Sterling Carlo Angiuli Daniel Gratzer |
| author_sort | Jonathan Sterling |
| collection | DOAJ |
| description | We present XTT, a version of Cartesian cubical type theory specialized for
Bishop sets \`a la Coquand, in which every type enjoys a definitional version
of the uniqueness of identity proofs. Using cubical notions, XTT reconstructs
many of the ideas underlying Observational Type Theory, a version of
intensional type theory that supports function extensionality. We prove the
canonicity property of XTT (that every closed boolean is definitionally equal
to a constant) using Artin gluing. |
| first_indexed | 2024-04-25T01:33:41Z |
| format | Article |
| id | doaj.art-af7976b79d7a4b4f97c8cb7067b80b13 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:33:41Z |
| publishDate | 2022-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-af7976b79d7a4b4f97c8cb7067b80b132024-03-08T10:36:54ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742022-03-01Volume 18, Issue 110.46298/lmcs-18(1:43)20229069A Cubical Language for Bishop SetsJonathan Sterlinghttps://orcid.org/0000-0002-0585-5564Carlo Angiulihttps://orcid.org/0000-0002-9590-3303Daniel Gratzerhttps://orcid.org/0000-0003-1944-0789We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets \`a la Coquand, in which every type enjoys a definitional version of the uniqueness of identity proofs. Using cubical notions, XTT reconstructs many of the ideas underlying Observational Type Theory, a version of intensional type theory that supports function extensionality. We prove the canonicity property of XTT (that every closed boolean is definitionally equal to a constant) using Artin gluing.https://lmcs.episciences.org/9069/pdfcomputer science - logic in computer sciencemathematics - logic |
| spellingShingle | Jonathan Sterling Carlo Angiuli Daniel Gratzer A Cubical Language for Bishop Sets Logical Methods in Computer Science computer science - logic in computer science mathematics - logic |
| title | A Cubical Language for Bishop Sets |
| title_full | A Cubical Language for Bishop Sets |
| title_fullStr | A Cubical Language for Bishop Sets |
| title_full_unstemmed | A Cubical Language for Bishop Sets |
| title_short | A Cubical Language for Bishop Sets |
| title_sort | cubical language for bishop sets |
| topic | computer science - logic in computer science mathematics - logic |
| url | https://lmcs.episciences.org/9069/pdf |
| work_keys_str_mv | AT jonathansterling acubicallanguageforbishopsets AT carloangiuli acubicallanguageforbishopsets AT danielgratzer acubicallanguageforbishopsets AT jonathansterling cubicallanguageforbishopsets AT carloangiuli cubicallanguageforbishopsets AT danielgratzer cubicallanguageforbishopsets |