English

Martin-L\"of Complexes

Logic 2012-05-25 v2 Category Theory

Abstract

In this paper we define Martin-L\"{o}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\"{o}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\"{o}f complexes and that this category is Quillen equivalent to the category of groupoids. In particular, 1-truncated Martin-L\"{o}f complexes are a model of homotopy 1-types.

Keywords

Cite

@article{arxiv.0906.4521,
  title  = {Martin-L\"of Complexes},
  author = {Steve Awodey and Pieter Hofstra and Michael A. Warren},
  journal= {arXiv preprint arXiv:0906.4521},
  year   = {2012}
}

Comments

44 pages; significant revisions

R2 v1 2026-06-21T13:17:26.276Z