Homotopy Theoretic Models of Type Theory
Logic
2012-08-30 v2 Algebraic Topology
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.
Cite
@article{arxiv.1208.5683,
title = {Homotopy Theoretic Models of Type Theory},
author = {Peter Arndt and Chris Kapulkin},
journal= {arXiv preprint arXiv:1208.5683},
year = {2012}
}
Comments
Corrected version of the published article