Model structures on categories of models of type theories

摘要

Models of dependent type theories are contextual categories with some additional structure.rnWe prove that if a theory T has enough structure, then the category T-Mod of its modelsrncarries the structure of a model category. We also show that if T has Σ-types, then weakrnequivalences can be characterized in terms of homotopy categories of models.