Model Structures on Categories of Models of Type Theories
Valery Isaev

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 has enough structure, then the category of its models carries the structure of a model category. We also show that if has types, then weak equivalences can be characterized in terms of homotopy categories of models.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
