依赖类型理论中严格相等的 coherence

我们研究通过附加严格相等扩展依赖类型理论的coherence与保守性。通过考虑类型理论模型的同余与商的概念,我们重构了Hofmann关于外延类型理论相对于内涵类型理论的保守性的证明。我们将这些方法推广到没有恒等式证明唯一性原理的类型理论,例如同伦类型理论的变体,通过引入类型理论模型上的高阶同余概念。我们对高阶同余的定义受Brunerie的弱∞-群胚的类型论定义启发。对于一大类类型理论,我们将等式扩展的保守性问题归约为更易处理的非循环条件。