2020/03/03 by Jonathan Sterling, Carlo Angiuli, Daniel Gratzer · 1 voice
Computer Science · Mathematics · #cs.LO #math.LO
paper · pdf · doi:10.46298/lmcs-18(1:43)2022
arxiv published 2020/03/03 · arxiv updated 2022/03/28
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.