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) by Artin gluing.
翻译:我们展示了一种为Bishop sets à la Coquand 专门设计的笛卡尔式立方体理论的版本XTT, 其中每种类型都享有身份证明的独特性的定义版本。 XTT 利用立方概念重建了许多观察类型理论的基本理念, 这是一种支持功能扩展性的强化型理论的版本。 我们证明了XTT( 每一个闭合的布尔在定义上都等同于恒定值) 的 canonicity 属性 。