Aarhus University Seal

A cubical language for bishop sets

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

  • Jonathan Sterling
  • ,
  • Carlo Angiuli, Carnegie Mellon University
  • ,
  • Daniel Gratzer

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 languageEnglish
JournalLogical Methods in Computer Science
Volume18
Issue1
Pages (from-to)43:1-43:80
Number of pages80
ISSN1860-5974
DOIs
Publication statusPublished - Mar 2022

    Research areas

  • Artin gluing, Bishop sets, cubical type theory, logical predicates, proof irrelevance

See relations at Aarhus University Citationformats

ID: 282003363