论文标题
$ \ infty $ -type理论的标准化和连贯性
Normalization and coherence for $\infty$-type theories
论文作者
论文摘要
我们开发了一种用于$ \ infty $ type理论的标准化技术。标准化属性有助于我们证明连贯定理：给定$ \ infty $ -type理论的初始模型为$ 0 $截断。连贯定理证明以$（\ infty，1）$ - 分类结构来解释普通类型理论是合理的。
We develop a technique for normalization for $\infty$-type theories. The normalization property helps us to prove a coherence theorem: the initial model of a given $\infty$-type theory is $0$-truncated. The coherence theorem justifies interpreting an ordinary type theory in $(\infty, 1)$-categorical structures.
