面向Bishop集的立方语言
A Cubical Language for Bishop Sets
AI总结：
提出XTT，一种面向Bishop集的笛卡尔立方类型理论，赋予类型同一性证明唯一性的定义性版本，并利用Artin粘合证明其规范性。
摘要：
我们提出XTT，一种为Coquand风格的Bishop集特化的笛卡尔立方类型理论版本，其中每个类型都享有同一性证明唯一性的定义性版本。利用立方概念，XTT重构了观测类型理论（一种支持函数外延性的内涵类型理论版本）的许多思想。我们使用Artin粘合证明了XTT的规范性（即每个封闭布尔值在定义上等于一个常量）。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
