Algebraic models of homotopy types and the homotopy hypothesis

TL;DR

This paper develops algebraic models called cylinder coherators for weak infinity groupoids, establishing their equivalence to spaces and proposing a framework compatible with type theory, advancing the understanding of homotopy types.

Contribution

It introduces a flexible notion of cylinder coherator, constructs semi-model categories of weak infinity groupoids, and links these models to the homotopy hypothesis and type theory.

Findings

All semi-model categories are Quillen equivalent and Quillen to spaces.

Explicit examples include simplicial and globular set-based models.

A conjecture is proposed that implies the Grothendieck homotopy hypothesis.

Abstract

We introduce and study a notion of cylinder coherator similar to the notion of Grothendieck coherator which define more flexible notion of weak infinity groupoids. We show that each such cylinder coherator produces a combinatorial semi-model category of weak infinity groupoids, whose objects are all fibrant and which is in a precise sense "freely generated by an object". We show that all those semi model categories are Quillen equivalent together and Quillen to the model category of spaces. A general procedure is given to produce such coherator, and several explicit examples are presented: one which is simplicial in nature and allows the comparison to the model category for spaces. A second example can be describe as the category of globular sets endowed with "all the operations that can be defined within a weak type theory". This second notion seem to provide a definition of weak infinity groupoids which can be defined internally within type theory and which is classically equivalent to homotopy types. Finally, the category of Grothendieck infinity groupoids for a fixed Grothendieck coherator would be an example of this formalism under a seemingly simple conjecture whose validity is shown to imply Grothendieck homotopy hypothesis. This conjecture seem to sum up what needs to be proved at a technical level to ensure that the theory of Grothendieck weak infinity groupoid is well behaved.