(Disclaimer: I'm no expert in homotopy theory nor in higher categories!) If I understand it correctly, Grothendieck's homotopy hypothesis states that there should be an equivalence (of $(n+1)$-categories) between "homotopy $n$-types" and $n$-groupoids. Where, by "homotopy $n$-types" is probably meant the $(\infty,n+1)$-category that has (nice) topological spaces with vanishing homotopy groups above the $n$-th as objects, and higher morphisms given by homotopies and homotopies-between-homotopies etc. And by "$n$-groupoid" is probably understood $(\infty,n)$-groupoid.

Edit: the homotopy types probably are defined to be some localization of the thing I stated above?

To which extent has the homotopy hypothesis been proved? By "proved" I mean precise statements and rigorous proofs, not just "philosophical" evidence; and not "tautological" solutions in which homotopy types are defined to be $\infty$-groupoids in the first place.

All this fits in the context of Whitehead's algebraic homotopy programme

Which is the present status of that programme, both in the sense of formalization and of proof?

How can any advance in the programme be made at all if Grothendieck's conjecture is not fully proven first?

  • 2
    $\begingroup$ I don't think your use of "(infty, n)" agrees with convention. I think by n-groupoid and n-category he really means... n-groupoid and n-category, in current parlance. $\endgroup$ Apr 9, 2017 at 11:39
  • 2
    $\begingroup$ Assuming that you formalize Whitehead's programme as an existence of fully faithful embedding of HoTop into some algebraic 1-category (i.e. algebras over some monad on $Set$), it can be proved impossible. See this paper of Peter Freyd. This means that basically any algebraic formalism that you use must be at least as complicated as spaces themselves, so defining n-groupoids as n-types is more or less required. The best you can do is choose some more tractable presentation of spaces, like simplicial sets or cubical sets or something. $\endgroup$ Apr 9, 2017 at 13:08
  • 3
    $\begingroup$ n-groupoid should mean an $(n,0)$-category, or an $(\infty, 0)$-category which represents it. Homotopy n-types themselves form an $(\infty, 1)$-subcategory of the $(\infty,1 )$-category of spaces, since there are no non-invertible $n>2$-morphisms between them. $\endgroup$ Apr 9, 2017 at 13:11

2 Answers 2


The problem is that the question is highly dependent on the definition of $n$-groupoids. The notion of strict $n$-groupoid is very clear and precise but we know very well (and Grothendieck knew that) that the homotopy hypothesis is false if we only use strict groupoids.

One needs to use weak $n$-groupoids (where for example composition is associative up to isomorphism and so one). But there is not a unique definition of what an $n$-groupoids is. There are plenty of non-equivalent definitions, which are supposed to become equivalent once we move to "homotopy categories".

For example, even for $2$-groupoids, you could ask to have a binary composition operation that composes two (composable) arrows and satisfies associativity up to isomorphism, plus the coherence condition between the associativity isomorphisms, or, follow the "unbiased" path and have for each $n$ a $n$-ary composition operation that compose string of (composable) $n$ arrows plus compatibility isomorphisms between these operations. The two approaches are not strictly equivalent, but will produce the same "homotopy category" (i.e. will be equivalent if one only considers groupoids up to categorical equivalence).

For example, taking "Kan complex" as a definition of $\infty$-groupoids can be considered as a reasonable choice and not as you said a "tautological solutions in which homotopy types are defined to be $\infty$-groupoids in the first place":

In a Kan complex, you do have a notion of $n$-morphisms and you can compose them and so on. It is a purely algebraic notion so to some extent I guess it could be considered an answer to the Whitehead program, depending on how you interpret the vague formulation given on the link you mention. Finally, the equivalence between the homotopy category of spaces and of Kan complexes is a rather non trivial result relying on an "algebraic approximation" result (the "simplicial approximation theorem").

(My understanding of history is that the realization that one can do homotopy theory purely algebraically using simplicial sets follows from Kan's work in the 50's, so a few years after Whitehead ICM talk, but I don't know much about it, so maybe someone would clarify this ? )

In Pursuing Stacks, Grothendieck did gave a different definition of $\infty$-groupoid, which follow a "globular" combinatorics, i.e. where instead of simplex as in Kan complexes, one has just have a notion of $n$-arrows between each pair or parallel $n-1$-arrows and operations on those. By the "homotopy hypothesis" one often refer to the statement that the homotopy category of Grothendieck $\infty$-groupoids is equivalent to the homotopy category of spaces. (see G.Maltsiniotis paper on this )

This version of the homotopy hypothesis is still widely open.

On the other hand, a proof of this version of the homotopy hypothesis does not seem that it would provide a better answer to the Whitehead program than a Kan complex: it is basically not easier to compute homotopy classes of maps with globular $\infty$-groupoids that it is with Kan complexes. The only difference between the two is the type of combinatorics that you have to describe your $n$-arrows and the relations between them. A bit in the same vein as the example I gave in the beginning with $2$-groupoids.

Finally, if I'm allowed to quote my own work (which I think bring some light on the question) in a recent paper I gave a different definition of $\infty$-groupoid, which is still globular (i.e. where you just have a collection of $n$-arrows between each pair of parallel $n-1$-arrows and some operation one those) but for which one can prove the homotopy hypothesis. These groupoids can be defined informally as globular sets equipped with all the operations than you can construct on a type in a weak version of intentional type theory.

I also proved in the same paper that Grothendieck formulation of the homotopy hypothesis is implied by some technical conjecture on the behavior of homotopy group of finitely generated Grothendieck $\infty$-groupoids, which can be dually understood as the fact that certain operation that you should be able to perform on arrows in a $\infty$-groupoid can indeed be defined from the operations Grothendieck puts on his $\infty$-groupoids (because map between finitely generated object, are the same as operations...).

I believe that my results show that our inability to prove Grothendieck's formulation of the homotopy hypothesis has nothing to do with an inability to express homotopy type as $\infty$-groupoids, but rather with some technical combinatorial difficulties inherent to Grothendieck's definition (basically, that it is not totally clear yet if Grothendieck's definition of $\infty$-groupoid is 'correct' and well behaved).

  • 2
    $\begingroup$ I don't think it's really correct to call Kan complexes a "purely algebraic notion". Algebraic notions are given by operations, whereas the definition of Kan complex includes axioms "for every horn there exists a (non-specified) filler". Using AC one may choose fillers, but they will not be preserved by morphisms of Kan complexes, while morphisms of "algebraic" structures preserve all the operations. So I think the closest one can come to a "purely algebraic notion" from this direction is "algebraic Kan complexes", whose homotopy hypothesis is also true: arxiv.org/abs/1003.1342 $\endgroup$ Nov 26, 2018 at 14:10
  • 1
    $\begingroup$ @MikeShulman : to me kan complex are endowed with chosen lift (because either you assume and you don't care, or you don't assume choice and you will need this assumption) and what you are refering to is only a distinction between considering $\infty$-groupoids with strict functors between them, or with pseudo-functors between them. But I definitely agree this is debatable.... And anyway the issue is solved by Nikolaus' paper. $\endgroup$ Nov 26, 2018 at 19:31
  • $\begingroup$ Simon, do we know the homotopy hypothesis yet for Grothendieck's definition of $\infty$-groupoid? I vaguely recall progress, but not enough to remember where and what. $\endgroup$
    – David Roberts
    Aug 21, 2020 at 2:09
  • $\begingroup$ No still not. except the result I mentioned in this post, the only new things is the construction by Lanari of the model structure for Grothendieck 3-groupoids (arxiv.org/abs/1809.07923) and a joint paper of Lanari and I where we generalize the result mentioned above to a proof that the existence of the "folk" model struture on n-groupoids implies the version of homotopy hypothesis for n-groupoids (arxiv.org/abs/1905.05625). Together, they proove the homotopy hypothesis for 3-groupoids, which is nice, but not so striking as this was already know... $\endgroup$ Aug 21, 2020 at 22:03
  • $\begingroup$ ... for stricter version of $3$-groupoids, like Gray-groupoids. Finally, I don't know if I should mention it (because it is still a bit speculative) but last summer Christopher Dean announced in a talk new results about constructing an "$\infty$-category of $\infty$-category" that might (if I understood his talk correctly) be enough to finish the proof of the homotopy hypothesis following my previous work, but these are not out yet, so I don't know yet. So... there is still some hope for a proof in the near future. $\endgroup$ Aug 21, 2020 at 22:12

I think this question is an interesting one, and the two approaches should be compared. I have more knowledge of Whitehead's programme, and have been involved with others in the development of aspects of that programme. A report on the background of part that work is in the paper Modelling and Computing Homotopy Types: I, to appear in 2017 in a special issue of Indagationes Mathematicae in honor of L.E.J. Brouwer. A notable feature of this work is that it deals not with "bare" spaces but with "Topological Data", and this somewhat reflects Grothendieck's view expressed in "Esquisse d'un Programme" Section 5. Also among the aims of Whitehead's work was to introduce invariants which allowed specific calculation and even if possible enumeration.

I should explain that having from 1965 to 1974 tried to define for a space $X$ a strict homotopy double groupoid which could satisfy a van Kampen type Theorem, and so enable specific calculations, it was a considerable relief to find with Philip Higgins that this could be done in a natural and intuitive way for a pair $(X,A,c)$ of pointed spaces by mapping the square $I^2$ into $X$ so that the edges of $I^2$ mapped to $A$ and the vertices mapped to $c$. This gave a vast generalisation of a tricky theorem on free crossed modules, proved in Section 16 of the 1949 paper "Combinatorial Homotopy II" (CHII).

Further this definition of homotopy double groupoid generalised, with considerable more work, to all dimensions using filtered spaces, so continuing Whitehead's programme in CHII.

The algebraic data used here of strict cubical $\omega$-groupoids, and the equivalent crossed complexes, do not model all homotopy types, and indeed contain in essence only "linear" information, i.e. no Whitehead products, for example. However these models do contain more information than chain complexes with a group of operators, conforming with an observation of Whitehead in CHII.

However a meeting with J.-L. Loday in 1981 in Strasbourg started our link with his work on what he called $n$-cat-groups, and we later agreed to call cat$^n$-groups, and which are $n$-fold groupoids in which one direction is a group. Loday had proved in 1982 modelled pointed homotopy $(n+1)$-types. We conjectured then and eventually proved a van Kampen type theorem in the context of $n$-cubes of spaces; this work was eventually accepted for the journal Topology, and a companion paper was accepted for Proc. London Math Soc, both appearing in 1987. The latter paper proved an $n$-adic Hurewicz Theorem, the triadic version of which was a conjecture of Loday in 1981.

Actually Grothendieck objected to the pointed condition, and did not recognise what had been achieved - he always wanted the most general conditions! However one aspect of the work with Loday, a nonabelian tensor product of groups which act on each other, has been well taken up by group theorists, and a current bibliography has 158 items dating from 1952.

H.-J. Baues in several books has continued aspects of Whitehead's programme, but he does not apply the Brown-Loday work, and his models do not satisfy the Criteria set out in Section 1 of the cited paper "Modelling and Computing Homotopy Types:I". However paper II of that has been delayed for various health reasons.

This paper, in a volume in memory of J.F.Adams, refers to work of G.J.Ellis and R. Steiner which applies the Brown-Loday work to solve an old problem in homotopy theory, on which Whitehead had written, to determine the value of the critical (i.e. first non vanishing) group of an $(n+1)$-ad.

Looking again at Esquisses d'un Progamme, it seems that programme has currently little relation to Whitehead's; but a 1983 letter from Grothendieck to the writer, reprinted as Problem 16.1.29 of Nonabelian Algebraic Topology, may suggest that despite his interest in the 2-d van Kampen theorem, the lack of progress with the issues he there raises indicates a limitation of this writer.

Grothendieck was very interested at one point in the idea I once conveyed to him that $n$-fold groupoids model homotopy $n$-types. But this is not true as stated even for $n=2$, since $2$-fold groupoids can be much more complicated than crossed modules over groupoids, which are a good model of homotopy $2$-types, and are equivalent to a special kind of double groupoid.

Added 18/04/2017: A final remark is that in my work with Higgins the cubical aspect is essential, and analogous results have not been obtained by simplicial methods. However the work with Loday does use also advanced simplicial methods for the proof of the main result. In both cases, the cubical methods are used to express multiple compositions, which are tricky simplicially.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.