论文标题
主教套装的立方语言
A Cubical Language for Bishop Sets
论文作者
论文摘要
我们提出XTT，这是专门用于主教的笛卡尔立方体类型理论的版本，其中每种类型都享有身份证明独特性的定义性版本。 XTT使用立方体概念重建了观察类型理论的许多思想，这是支持功能扩展性的强化类型理论的一种版本。我们使用Artin Gluing证明了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.
