arXiv · 0906.4521
Martin-Löf Complexes
Abstract
In this paper we define Martin-Löf complexes to be algebras for monads on the category of (reflexive) globular sets which freely add cells in accordance with the rules of intensional Martin-Löf type theory. We then study the resulting categories of algebras for several theories. Our principal result is that there exists a cofibrantly generated Quillen model structure on the category of 1-truncated Martin-Löf complexes and that this category is Quillen equivalent to the category of groupoids. In particular, 1-truncated Martin-Löf complexes are a model of homotopy 1-types.
Explore related subjects
Keep this discovery
Steve Awodey, Pieter Hofstra, Michael A. Warren. 2012-05-24. Martin-Löf Complexes. https://arxiv.org/abs/0906.4521
Cite the original work for its findings. Save a collection to share your selection of sources.