相依类型论中严格等式的相合性
Coherence of strict equalities in dependent type theories
摘要：
利用附加的严格等式研究了相关类型论扩张的凝聚性和保守性。通过考虑类型论模型的同馀项和同馀项的概念，我们重建了Hofmann关于外延类型论相对于内涵类型论的保守性的证明.我们推广这些方法的类型论没有统一的身份证明原则，如变种同伦类型论，通过引入一个概念，更高的同余模型的类型论。我们对更高全等的定义受到Brunerie对弱$\infty$ -群胚的类型论定义的启发。对于一个大类的类型论，我们减少了问题的保守性方程扩展到更易处理的无环性条件。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
