Homotopy-Theoretic Models of Type Theory

摘要

We introduce the notion of a logical model category, which is a Quillen model category satisfying some additional conditions. Those conditions provide enough expressive power that one can soundly interpret dependent products and sums in it while also having a purely in-tensional interpretation of the identity types. On the other hand, those conditions are easy to check and provide a wide class of models that are examined in the paper.