A Cubical Language for Bishop Sets
Logic in Computer Science
2023-06-22 v5 Logic
Abstract
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.
Cite
@article{arxiv.2003.01491,
title = {A Cubical Language for Bishop Sets},
author = {Jonathan Sterling and Carlo Angiuli and Daniel Gratzer},
journal= {arXiv preprint arXiv:2003.01491},
year = {2023}
}