标题： 类型理论模型范畴上的模型结构 显示英文标题

标题： Model Structures on Categories of Models of Type Theories

摘要： 依赖类型理论的模型是具有某些额外结构的上下文范畴。 我们证明，如果理论$T$具有足够的结构，那么其模型范畴$T\text{-}\mathbf{Mod}$具有模型范畴的结构。 我们还表明，如果$T$具有$\Sigma$类型，那么弱等价可以借助模型的同伦范畴来表征。 显示英文摘要

摘要： Models of dependent type theories are contextual categories with some additional structure. We prove that if a theory $T$ has enough structure, then the category $T\text{-}\mathbf{Mod}$ of its models carries the structure of a model category. We also show that if $T$ has $\Sigma$ types, then weak equivalences can be characterized in terms of homotopy categories of models.