Model Structures on Categories of Models of Type Theories

TL;DR

This paper explores the structure of categories of models of dependent type theories, demonstrating they can form model categories under certain conditions and characterizing weak equivalences via homotopy categories.

Contribution

It establishes conditions under which categories of models of type theories form model categories and characterizes weak equivalences when $\Sigma$ types are present.

Findings

Categories of models of certain type theories can be endowed with a model category structure.

Weak equivalences in these categories can be characterized using homotopy categories when $\Sigma$ types exist.

Provides a framework linking dependent type theories with homotopical algebra.

Abstract

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.