型论弱分解系统

摘要：

本文给出了σ-完备范畴上的弱分解系统的三个刻画，它们分别用Sigma-、Pi-和Id-类型解释内涵依赖类型理论.第一个刻画是弱分解系统（L，R）具有如下性质：L在沿R的拉回下是稳定的，且所有到终对象的映射都在R中。我们称这样的弱分解系统为类型论的。第二个是弱分解系统有一个Id-表示：大致上，它是由空上下文中的Id-类型生成的。第三，弱分解系统（L，R）是由Moore关系系统生成的，Moore关系系统是Moore路概念的推广。

英文摘要：

This article presents three characterizations of the weak factorization systems on finitely complete categories that interpret intensional dependent type theory with Sigma-, Pi-, and Id-types. The first characterization is that the weak factorization system (L,R) has the properties that L is stable under pullback along R and that all maps to a terminal object are in R. We call such weak factorization systems type-theoretic. The second is that the weak factorization system has an Id-presentation: roughly, it is generated by Id-types in the empty context. The third is that the weak factorization system (L, R) is generated by a Moore relation system, a generalization of the notion of Moore paths.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。