Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review
Final published version
We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets à 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.
Original language | English |
---|---|
Journal | Logical Methods in Computer Science |
Volume | 18 |
Issue | 1 |
Pages (from-to) | 43:1-43:80 |
Number of pages | 80 |
ISSN | 1860-5974 |
DOIs | |
Publication status | Published - Mar 2022 |
See relations at Aarhus University Citationformats
ID: 282003363