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 |
| Summary: | 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. |
|---|---|
| ISSN: | 1860-5974 |