一句话：提出 XTT——面向 Bishop 集合的笛卡尔立方类型论，使所有类型满足定义性 UIP，并证明 canonicity。
本文提出 XTT，一种为 Coquand 意义下的 Bishop 集合定制的笛卡尔立方类型论。其核心特征是每个类型均满足定义性版的同一性证明唯一性（UIP），从而在内涵类型论中恢复外延性质。XTT 借助立方结构重构了观察型类型论（OTT）的若干思想，并支持函数外延性。作者使用 Artin gluing 证明 XTT 的 canonicity：每个闭布尔值都定义地等于 true 或 false。该工作展示了如何将立方方法用于 Bishop 集合，并为定义性 UIP 与函数外延性提供统一的类型论框架。
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) using Artin gluing.
@article{paperbot1711,
title = {A Cubical Language for Bishop Sets},
author = {Jonathan Sterling and Carlo Angiuli and Daniel Gratzer},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:43)2022}
}