2016/07/25 by Isaev, Valery
#Category Theory (math.CT) #FOS: Mathematics
paper · doi:10.48550/arxiv.1607.07407
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-Mod of its models carries the structure of a model category. We also show that if T has Σ types, then weak equivalences can be characterized in terms of homotopy categories of models.