Martin-L\"of Complexes

TL;DR

This paper introduces Martin-Löf complexes as algebraic structures modeling intensional Martin-Löf type theory, establishing a Quillen model structure on 1-truncated complexes that corresponds to homotopy 1-types.

Contribution

It defines Martin-Löf complexes as algebras for specific monads and proves a Quillen equivalence with groupoids for 1-truncated cases, linking type theory and homotopy theory.

Findings

Existence of a cofibrantly generated Quillen model structure on 1-truncated Martin-Löf complexes.

Quillen equivalence between 1-truncated Martin-Löf complexes and groupoids.

Martin-Löf complexes model homotopy 1-types.

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.