论文标题
在依赖类型理论中严格平等的一致性
Coherence of strict equalities in dependent type theories
论文作者
论文摘要
我们通过额外的严格平等研究研究了依赖类型理论的扩展的连贯性和保守性。通过考虑类型理论模型的一致性和商的概念，我们重建了霍夫曼（Hofmann）对强度类型理论的延伸类型理论的保守性证明。我们将这些方法推广到没有身份证明原则的独特性（例如同型类型理论的变体）的键入理论的概括，这是通过对类型理论模型的较高一致性的概念引入更高的一致性的概念。我们对较高一致性的定义灵感来自Brunerie对弱$ \ infty $ groupoid的类型理论定义。对于大量类型的理论，我们将方程扩展的保守性问题减少到更可行的环境条件。
We study the coherence and conservativity of extensions of dependent type theories by additional strict equalities. By considering notions of congruences and quotients of models of type theory, we reconstruct Hofmann's proof of the conservativity of Extensional Type Theory over Intensional Type Theory. We generalize these methods to type theories without the Uniqueness of Identity Proofs principle, such as variants of Homotopy Type Theory, by introducing a notion of higher congruence over models of type theory. Our definition of higher congruence is inspired by Brunerie's type-theoretic definition of weak $\infty$-groupoid. For a large class of type theories, we reduce the problem of the conservativity of equational extensions to more tractable acyclicity conditions.
