一句话：提出 TTobs，为依赖类型论中每个类型配备满足函数外延、命题外延和 UIP 的同一关系，并证明规范化、正则性与可判定性。
依赖类型论若加入函数外延、命题外延和 UIP 等原则，常会破坏归约与判定性。本文在带定义性证明无关类型宇宙的依赖类型论基础上，提出基于集合式（setoidal）解释的类型论 TTobs。它为每个类型配备同一关系，并满足函数外延、命题外延及定义性 UIP。相比已有方案，TTobs 的归约可规范化，并具有算法性正则性；作者利用 Abel 等人的逻辑关系框架在 Agda 中形式化证明。还给出转换与类型检查可判定性及一致性，并说明如何加入商类型，以及引入 Swan Id 类型的集合式版本，使其成为带归纳等式的 MLTT 扩展。
Building on the recent extension of dependent type theory with a universe of definitionally proof-irrelevant types, we introduce TTobs, a new type theory based on the setoidal interpretation of dependent type theory. TTobs equips every type with an identity relation that satisfies function extensionality, propositional extensionality, and definitional uniqueness of identity proofs (UIP). Compared to other existing proposals to enrich dependent type theory with these principles, our theory features a notion of reduction that is normalizing and provides an algorithmic canonicity result, which we formally prove in Agda using the logical relation framework of Abel et al. Our paper thoroughly develops the meta-theoretical properties of TTobs, such as the decidability of the conversion and of the type checking, as well as consistency. We also explain how to extend our theory with quotient types, and we introduce a setoidal version of Swan's Id types that turn it into a proper extension of MLTT with inductive equality.