A Cubical Language for Bishop Sets

Abstract

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.

References in corpus (3)

• Higher Topos Theory
• Normalization for Cubical Type Theory
• Notes on Clans and Tribes

Cited by in corpus (3)

• Normalization for Cubical Type Theory
• An extensible equality checking algorithm for dependent type theories
• Logical Relations as Types: Proof-Relevant Parametricity for Program Modules