The homotopy hypothesis is the assertion that
or rather the stronger statement that
and moreover
What this actually means in detail depends on which definition of ∞Grpd is being used and to which precise incarnation of Top it is being compared to.
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 $\infty$-groupoids is located, the statement may be more or less obvious.
For instance there is some justification for defining an $\infty$-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 $\infty$-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 $\infty$-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 $\infty$-groupoids not much indication for how to prove the homotopy hypothsis 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 $\infty$-groupoids is hoped/required to reproduce this, and hence is hoped/required to satisfy the homotopy hypothesis.
Apart from having different models of $\infty$-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 $\infty$-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).
We discuss various different definitions of n-groupoids and ∞-groupoids and the formulation and proof of the homotopy hypothesis for them, to the extent that it is available.
The 2-category Grpd of groupoids, functors, and natural transformations is equivalent to the 2-category of homotopy 1-types, continuous maps, and homotopy classes of homotopies.
(…) 2-groupoids model all homotopy 2-types (…)
strict 2-groupoids suffice (…) (but note that strict 2-functors are not sufficient to model all maps between 2-types)
(…) Gray-groupoids model all homotopy 3-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.
(…)
We write $sSet_{Quillen}$ for sSet equipped with the standard model structure on simplicial sets. The cofibrant-fibrant objects in $sSet_{Quillen}$ are precisely the Kan complexes.
Also we write $Top_{Quillen}$ for Top equipped with the standard model structure on topological spaces.
There is a Quillen equivalence
where the left adjoint $|-|$ is geometric realization and the right adjoint $Sing(-)$ is forming the singular simplicial complex $Sing(-)$.
This induces an equivalence of (∞,1)-categories of the corresponding presented (∞,1)-categories
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.
Algebraic Kan complexes constitute a genuine algebraic model in that they are precisely the algebras over a monad on sSet.
The transferred model structure on algebraic Kan complexes is Quillen equivalent to the standard model structure on simplicial sets
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 $Alg Kan$ and $Top$
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:
Write $\Delta^n$ and $\Lambda^n_k$ for the topological $n$-simplex and its $k$-horn.
Fix any choice of retracts
for all topological horn inclusions $\Lambda^n_i \hookrightarrow \Delta^n$.
For $X$ any topological space equip the singular simplicial complex $Sing X$ with the stucture of an algebraic Kan complex by taking the filler of $\Lambda_k[n] \to Sing X$ to be given by the $(|-| \dashv Sing)$-adjunct of $\Delta^n \stackrel{R(n,k)}{\to} \Lambda^n_k \to X$. Write $\Pi_\infty(X) \in Alg Kan$ for the resulting algebraic Kan complex.
This construction constitutes a functor
with $U \Pi_\infty = Sing$.
The choices of fillers in $\Pi_\infty(X)$ may be thought of as explicit choice of reparameterizations of paths in $X$. These choices are arbitrary, but by the general statement at model structure on algebraic fibrant objects, any two chocies yield equivalent objects.
Given choices $R(-,-)$ of horn retracts as above, define a functor
called reduced geometric realization by taking it on an object $A \in Alg Kan$ to be given by the coequalizer
where $|U A|$ is the ordinary geometric realization of the underlying simplicial set of $A$ and where the two maps are
the image under $|-|$ of the distinguished fillers $\Delta[n] \to U A$ of $A$;
the composite $\Delta^n \stackrel{R(n,k)}{\to} \Lambda^n_k \to |U X|$ .
This is (Nikolaus, prop. 3.4).
We check the hom-isomorphism. A morphism $f : |A|_r \to X$ is by definition of the coequalizer the same as a map $\tilde f : |A| \to X$ such that for each horn $h : \Lambda[n]_k \to A$ with distinguished filler $\hat h : \Delta[n] \to A$ the composites
and
are equal. This means equivalently that the $(|-| \dashv Sing)$-adjunct $\tilde \tilde f : U A \to Sing X$ sends distinguished fillers in $A$ to distinguished fillers in $\Pi_\infty(X)$ and is hence a morphism in $Alg Kan$.
the constructon shows that the map $(f : |A|_r \to X) \mapsto (\tilde \tilde f : A \to \Pi_\infty(X))$ 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 $\Pi_\infty$.
Using this, we have that
So $|-|_r \circ F$ is another left adjoint to $Sing$ and hence naturally isomorphism to $|-|$.
The adjunction
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.
There is an evident simplicial set-valued functor
from the cube category to sSet, which sends the cubical $n$-cube to the simplicial $n$-cube
Similarly there is a canonical Top-valued functor
The corresponding nerve and realization adjunction
is the cubical analogue of the simplicial nerve and realization discussed above.
There is a model structure on cubical sets $Set^{\Box^{op}}$ 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 $Set^{\Box}$ for every cubical set $A$.
The counit of the adjunction
is a weak equivalence in $Top$ for every topological space $X$.
It follows that we have an equivalence of categories induced on the homotopy categories
This is Jardine, theorem 29, corollary 30.
Loday’s notion of a cat-n-group corresponds to the connected version of an $n+1$-fold groupoid. We will restrict our discussion to that connected case.
The homotopy category of cat-n-groups is equivalent to that of pointed connected homotopy n+1-types.
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,
Its unit is an equivalence of Segal categories and its counit a weak homotopy equivalence of topological spaces.
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 $\omega$-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).
The issue however is somewhat subtle, as very much highlighted by Voevodsky here. For more on this see at Simpson's conjecture.
An introductory survey is given in
The original form of the homotopy hypothesis for Kan complexes is due to Dan Quillen. See the references at model structure on simplicial sets.
The homotopy hypothesis for strict $\omega$-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 $n$-types by $Cat^n$-groups are discussed in
More literature on models of homotopy types by strict higher groupoids is at
Ronnie Brown, Computing Homotopy Types Using Crossed $N$-Cubes of Groups (arXiv)
Simona Paoli, Internal categorical structures in homotopical algebra, to appear in Towards Higher Categories, eds. John Baez and Peter May (pdf)
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