Jonathan Sterling ; Carlo Angiuli ; Daniel Gratzer - A Cubical Language for Bishop Sets

lmcs:9069 - Logical Methods in Computer Science, March 29, 2022, Volume 18, Issue 1 - https://doi.org/10.46298/lmcs-18(1:43)2022
A Cubical Language for Bishop SetsArticle

Authors: Jonathan Sterling ORCID; Carlo Angiuli ORCID; Daniel Gratzer ORCID

    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.


    Volume: Volume 18, Issue 1
    Published on: March 29, 2022
    Accepted on: February 9, 2022
    Submitted on: February 9, 2022
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic

    Consultation statistics

    This page has been seen 1355 times.
    This article's PDF has been downloaded 420 times.