Martin-Löf Complexes

Details Martin-Löf Complexes Martin-Löf Complexes

2009-06-24

arxiv.org/abs/0906.4521v1

Mathematics

Logic

62 pages

Scientific paper

In this paper we define Martin-L\"of 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\"of 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\"of complexes and that this category is Quillen equivalent to the category of groupoids. In particular, 1-truncated Martin-L\"of complexes are a model of homotopy 1-types. In order to establish these facts we give a proof-theoretic analysis, using a modified version of Tait's logical predicates argument, of the propositional equality classes of terms of identity type in the 1-truncated theory.

Affiliated with

Also associated with

No associations

Rating

Martin-Löf Complexes does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Martin-Löf Complexes, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Martin-Löf Complexes will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-106461