Homotopy Theoretic Models of Type Theory

Abstract

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. On the other hand, those conditions are easy to check and provide a wide class of models some of which are listed in the paper.

Corrected version of the published article

References in corpus (7)

• Higher Topos Theory
• Polynomial functors and polynomial monads
• Homotopy theoretic models of identity types
• The identity type weak factorisation system
• Two-dimensional models of type theory
• On the strength of dependent products in the type theory of Martin-Löf
• Type theory and homotopy

Cited by in corpus (9)

• Univalent categories and the Rezk completion
• The Simplicial Model of Univalent Foundations (after Voevodsky)
• Univalence for inverse diagrams and homotopy canonicity
• Univalence in locally cartesian closed infinity-categories
• Univalence and completeness of Segal objects
• Topos and Stacks of Deep Neural Networks
• Synthetic Spectra via a Monadic and Comonadic Modality
• $(\infty ,1)$-Categorical Comprehension Schemes
• Limits and colimits of synthetic $\infty$-categories