Martin-L\"of Complexes
classification
🧮 math.LO
math.CT
keywords
martin-lcategorycomplexesalgebrasmodelquillentruncatedaccordance
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.