• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Article

Model structures on categories of models of type theories

Mathematical Structures in Computer Science. 2018. Vol. 28. No. 10. P. 1695-1722.
Valery Isaev.

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.