Carnegie Mellon University
Browse

Martin-Löf Complexes

Download (635.75 kB)
journal contribution
posted on 2009-06-25, 00:00 authored by Steven AwodeySteven Awodey, P. Hofstra, M. Warren
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.

History

Publisher Statement

All Rights Reserved

Date

2009-06-25

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC