1. Martin-Löf complexes.
- Author
-
Awodey, Steve, Hofstra, Pieter, and Warren, Michael A.
- Subjects
- *
ALGEBRA , *SET theory , *GROUPOIDS , *MATHEMATICAL category theory , *MATHEMATICAL complexes , *TYPE theory - 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. [ABSTRACT FROM AUTHOR]
- Published
- 2013
- Full Text
- View/download PDF