The homotopy hypothesis is the assertion that
or rather the stronger statement that
There are some definitions of ∞-groupoids for which the homotopy hypothesis is a proven theorem . Depending on where in the spectrum between geometric definitions of higher categories and algebraic definitions of higher categories a given definition of -groupoids is located, the statement may be more or less obvious.
For instance there is some justification for defining an -groupoid to be equivalently a topological space (considered modulo weak homotopy equivalence). For this definition the homotopy hypothesis is of course a tautology.
A definition of -groupoid that is still very geometrical but much more combinatorial is that given by Kan complexes. For these the homotopy hypothesis has a (non-trivial but fairly tractable) proof. The equivalence between Kan complexes and CW-complexes obtained this way is at the heart of all traditional homotopy theory.
A genuine algebraic definition of -groupoids for which the homotopy theory has a (non-trivial but tractable) proof is given by algebraic Kan complexes.
However for other algebraic definitions of -groupoids not much indication for how to prove the homotopy hypothesis is known. The definition of Trimble ω-category stands out as an algebraic definition that has the notion of fundamental ∞-groupoid built right into it, but also here it seems unclear at the moment how to make progress with proving the homotopy hypothesis.
In fact, generally the homotopy hypothesis is regarded as a consistency condition for definitions in higher category theory:
One way to justify this condition is by recourse to the proven cases of the homotopy hypothesis: experience shows that the collections of all three models – topological spaces, Kan complexes, algebraic Kan complexes – provide a model for ∞Grpd that supports the general abstract higher category theory – specifically (∞,1)-category theory – that one expects in analogy to how Set supports ordinary category theory. Any other definition of -groupoids is hoped/required to reproduce this, and hence is hoped/required to satisfy the homotopy hypothesis.
Apart from having different models of -groupoids that lend themselves more or less to a comparison with topological spaces, there is also the issue as to how to conceive of the notion of equivalence between -groupoids.
The usual, unstated, implication is that the notion of equivalence of n-groupoids used to model homotopy n-types is the appropriate n-category-theoretic notion of equivalence. It is in this way that, for instance, it is known that 1-groupoids model homotopy 1-types (see below).
The reason this is important to specify is that there are other notions of equivalence on categorical structures which model homotopy types in other ways. For example, if we declare a functor between categories to be a weak equivalence iff its nerve is a weak equivalence of simplicial sets, then all homotopy types can be modeled by 1-categories in this way; see the Thomason model structure for 1-categories.
Finally, in analogy to the homotopy hypothesis, there are also attempts to relate general (∞,n)-categories (not necessarily groupoidal) to directed topological spaces by a fundamental (∞,n)-category-construction. There have been claims that a directed homotopy hypothesis can be proven, but at the moment there does not seem to be a published statement.
The following general abstract statement of the homotopy hypothesis is often useful to make explicit.
This statement can be formulated, holds true and is proven below at least for the standard definitions of these two (∞,1)-categories (see section on Kan complexes, section on algebraic Kan complexes).
See homotopy hypothesis for 1-types for more.
strict 2-groupoids suffice (…) (but note that strict 2-functors are not sufficient to model all maps between 2-types)
It is known that not all homotopy 3-types can be modeled by strict 3-groupoids, but that Gray-categories (semi-strict 3-categories) suffice; the obstruction is the Whitehead product which arises from a nontrivial interchanger.
There is a Quillen equivalence
An algebraic Kan complex is an algebraic definition of higher groupoids obtained by taking the ordinary definition of Kan complex and equipping these with choices of horn-fillers. These choice encode specified composition operations, specified associators for these, specified pentagonators and so on.
The proof is spelled out at model structure on algebraic fibrant objects.
With the above homotopy hypothesis-theorem for Kan complexes this gives a zig-zag of Quillen equivalences between and
This already yields the homotopy hypothesis for algebraic Kan complexes at the level of the corresponding presented (∞,1)-categories (as discussed there)
But there is also a direct Quillen equivalence:
Fix any choice of retracts
for all topological horn inclusions .
For any topological space equip the singular simplicial complex with the stucture of an algebraic Kan complex by taking the filler of to be given by the -adjunct of . Write for the resulting algebraic Kan complex.
This construction constitutes a functor
The choices of fillers in may be thought of as explicit choice of reparameterizations of paths in . These choices are arbitrary, but by the general statement at model structure on algebraic fibrant objects, any two chocies yield equivalent objects.
Given choices of horn retracts as above, define a functor
called reduced geometric realization by taking it on an object to be given by the coequalizer
where is the ordinary geometric realization of the underlying simplicial set of and where the two maps are
the image under of the distinguished fillers of ;
the composite .
The functor is left adjoint to .
This is (Nikolaus, prop. 3.4).
We check the hom-isomorphism. A morphism is by definition of the coequalizer the same as a map such that for each horn with distinguished filler the composites
are equal. This means equivalently that the -adjunct sends distinguished fillers in to distinguished fillers in and is hence a morphism in .
the constructon shows that the map thus obtained is a bijection.
We have an identity
and a natural isomorphism
This is (Nikolaus, corollary 3.5)
The identity is evident by definition of .
Using this, we have that
So is another left adjoint to and hence naturally isomorphism to .
constitutes a Quillen equivalence
This is Nikolaus, corollary 3.6
By the above theorem and the 2-out-of-3-property of Quillen equivalences.
Also cubical sets may serve as a model for homotopy theory.
Similarly there is a canonical Top-valued functor
is the cubical analogue of the simplicial nerve and realization discussed above.
There is a model structure on cubical sets whose
weak equivalences are the morphisms that become weak equivalences under geometric realization ;
cofibrations are the monomorphisms.
This is Jardine, sections 3.
is a weak equivalence in for every cubical set .
The counit of the adjunction
is a weak equivalence in for every topological space .
This is Jardine, theorem 29, corollary 30.
Loday’s notion of a cat-n-group corresponds to the connected version of an -fold groupoid. We will restrict our discussion to that connected case.
This is proven in (Loday). (There are some glitches in his proof and these were fixed by various authors (Steiner, Gilbert, ..) and then detailed proofs were given by Bullejos, Cegarra, Duskin and separately, using the equivalent formulation of crossed n-cubes, by Porter. Detailed references and some more commentary is at cat-n-group.)
There is realization/singular complex adjunction
for Segal groupoids,
This is lemma 6.3.21 and corollary 6.3.24 in (Pellissier)
While strict omega-groupoids in the sense of strict omega-categories with strict inverses are far from modelling all homotopy types, strict -categories with all weak inverses come closer. In (Kapranov-Voevodsky) it was argued that these are in fact sufficient, but a mistake in the argument is claimed in (Simpson, cor. 5.2) (see also here).
An introductory survey is given in
The original form of the homotopy hypothesis for Kan complexes is due to
Textbook accounts include
The homotopy hypothesis for strict -categories with weak inverses is discussed in
but a mistake in the argument is claimed in cor 5.2 of
The homotopy hypothesis for algebraic Kan complexes is established and discussed in
The homotopy hypothesis for Segal groupoids is formulated in section 6.3.4 of
Models of homotopy -types by -groups are discussed in
More literature on models of homotopy types by strict higher groupoids is at
The first paper, as its title suggests, has an emphasis on using higher groupoids for computation of homotopical invariants, in fact by applying higher homotopy van Kampen Theorems. These theorems lead to algebraic colimit arguments in algebraic topology, implying results, often nonabelian, not obtainable by other methods. It is also remarkable that the precision of these results requires the use of strict structures, whereas the current emphasis in higher category theory is on non strict structures.
The homotopy theory of cubical sets is discussed in
Cubical methods are also essential in
A version for stratified spaces is discussed in