In the setting of Homotopy Type Theory, how would you construct $\mathrm{isStrict} : U \rightarrow U$ which is inhabited exactly when the first type is (equivalent to?) a strict $\infty$-groupoid?

The "obvious" (to me, at least) approach is that if you have a strict $\infty$-groupoid you want associativity to be a judgemental equality and not just a propositional equality. However, there's a major problem with that approach, which is that composition itself has many different definitions which are all propositionally equal but not judgementally equal. Furthemore, by univalence, you shouldn't be able to distinguish between the types which are strict $\infty$-groupoids and the types which are equivalent to strict $\infty$-groupoids. (Similarly, isSet actually detects the property of being a $0$-type instead of being a set.) So is there an alternative approach?

  • 5
    $\begingroup$ A related question to ask would be whether there is a notion of "strict object" definable in an arbitrary $(\infty,1)$-topos? If strict $\infty$-groupoids were definable in HoTT, then the definition would internalize to give a positive answer to this question. Conversely, a positive answer to this question might suggest the appropriate definition in HoTT. $\endgroup$ – Mike Shulman Oct 25 '13 at 5:14

I realize I'm dropping in long after all the excitement is over. However, I'd like to point out an implicit assumption which is (seemingly) inherent in the original question as well as some of the answers: namely, that "being strict" is a property of $\infty$-groupoids, rather than a structure put on an $\infty$-groupoid.

It is reasonable to suppose we have some kind of realization functor $$ \Re: St\infty Gpd \to \infty Gpd,$$ so that the homotopy groups of the space $\Re G$ naturally coincide with the homotopy groups of the strict infinty groupoid $G$. (This notion is due to Simpson, http://arxiv.org/abs/math/9810059).

Since there are notions of weak equivalence for both $\infty Gpd$ and $St\infty Gpd$, these both give (weak) $(\infty,1)$-categories, and $\Re$ is a functor between them. If $\Re$ happened to be fully faithful as a functor of $(\infty,1)$-categories, it would be reasonable to regard strictness as a property of $\infty$-groupoids. However, there no reason to think that is the case: being strict is not a property.

It is, of course, licit to ask "which $\infty$-groupoids are in the essential image of $\Re$", and to call that $\mathtt{isStrict}$. However, if $\Re$ is not fully faithful, then knowledge of $\mathtt{isStrict}$ is not at all the same as "defining strict infinity groupoids". (The same issue appears in Mike's variant involving the forgetful functor $H\mathbb{Z}Mod\to Spectra$.)

Actually, there is no need to speculate here. There are theorems:

  • The category $St\infty Gpd$ is equivalent to the category $Crs$ of "crossed-complexes" (Brown-Higgins, http://groupoids.org.uk/pdffiles/x-comp.pdf).

  • There is a closed model structure on $Crs$, where the weak equivalences are what you expect (Brown-Golasinski, http://groupoids.org.uk/pdffiles/RB-golskyrev.pdf; see also Ara-Metayer, http://arxiv.org/abs/1010.2599).

  • There is an adjoint pair $$ \pi\colon sSet \rightleftarrows Crs :N$$ where the "nerve" functor $N$ is an example of a realization functor $\Re$. Furthermore, this adjunction is a Quillen pair relating the Brown-Golasinski model structure on $Crs$ with the Kan-Quillen model structure on $sSet$. (Brown-Higgins, http://groupoids.org.uk/pdffiles/crossedcomplexclass.pdf; I don't think they say "Quillen pair", but they prove what is needed in section 6.)

  • The derived functor of $N$ is evidently not fully-faithful. In fact (Ara, http://arxiv.org/abs/1206.2945), the homotopy category of simply connected strict $\infty$-groupoids is equivalent to $\mathcal{D}_{\geq2}(Ab)$, and any realization functor takes such objects to the evident products of Eilenberg-MacLane spaces. There are many more maps between Eilenberg-MacLane spaces than come from the derived category, so no realization functor can be fully faithful.

It's still reasonable to ask if strictness is a structure on an $\infty$-groupoid (e.g., if $\Re$ is monadic in the $\infty$-categorical sense). For that matter, it's reasonable to ask if "weakness" is a structure on a strict $\infty$-groupoid (e.g., if the $\infty$-categorical left adjoint to $\Re$, modelled by $\pi$ in the Brown-Higgins paper, is comonadic). These seem like interesting questions.

Note: in the above, "strict $\infty$-groupoid" means a strict $\infty$-category in which all $k$-morphisms have inverses. There is also a more general notion of "quasistrict $\infty$-groupoid", in which $k$-morphisms have weak inverses. I gather less is known about these; see the paper by Ara referenced above.

  • $\begingroup$ Could you give an example of a map between Eilenberg-MacLane spaces $X$ and $Y$ such that the homotopy class of the map doesn't come from a map in $\mathcal{D}_{\geq 2}(\operatorname{Ab})(C^\bullet X,C^\bullet Y)$? I thought that this was the point of Eilenberg-MacLane spaces, but I guess I am very mistaken. $\endgroup$ – Harry Gindi Nov 5 '18 at 10:31
  • $\begingroup$ @HarryGindi Steenrod operations $\endgroup$ – Dylan Wilson Nov 5 '18 at 13:55
  • $\begingroup$ @CharlesRezk I computed a pseudofunctor for Str-$\infty$-Cat between Eilenberg-MacLane infty groupoids and showed that $\operatorname{Sq}^2$ can be obtained in this way. This appears to indicate that the main problem in Str-$\omega$-gpds is not the structure per se, but a faulty resolution. $\endgroup$ – Harry Gindi Nov 7 '18 at 8:03
  • $\begingroup$ In particular, Ho(Str-$\infty$-Gpd) into Ho(Str-$\infty$-Cat) is already not a full embedding. $\endgroup$ – Harry Gindi Nov 7 '18 at 8:04

There will be no way to do what you'd like inside homotopy type theory, where the only equality visible is propositional equality. You could move to meta-level and provide a meta-theoretic definition of a strict structure which involves judgmental equalities, but that brings a new kind of trouble with it.

Let me put it another way. Suppose you have a candidate isStrict that would describe "strict $\infty$-groupoids", whatever they are. If we manage to exhibit a a strict $\infty$-groupoid $X$ that is (homotopy) equivalent to a non-strict $\infty$-groupoid $Y$, then by the Univalence axiom $X = Y$ (in the propositional sense) and so isStrict would hold for the non-strict $Y$ as well. So I think that's going to be a real problem, because I would expect to be able to find such $X$ and $Y$, whatever the alleged "strict" and "non-strict" $\infty$-groupoids might be.

A similar but simpler situation requiring a bit of meta-level thinking about judgmental and propositional equality arises with the interval type. It is a higher inductive type generated by two points $0$ and $1$, and a path $\mathtt{seg} : 0 = 1$. Because the interval is contractible, it is equivalent to the singleton type $\mathtt{unit}$, so any statement in type theory which you make about the interval also holds for the singleton. But it would be wrong to conclude from this that the interval is useless. For example, its existence implies function extensionality. So what distinguished the interval from the singleton? The fact that $0 = 1$ propositionally but not judgmentally.

With a complicated structure, such as $\infty$-groupoids everything seems to be much more complicated, as it is not clear how to avoid talking about infinitely many "levels" of structure.

To deal with constructions where one wants strict equality as well as the "homotopy" one, Vladimir Voevodsky proposed that a type system with two kinds of equality be developed. If you do this naively then you can prove that the two equalities are in fact equivalent, so something not so naive must be done. So perhaps in the future we will have a type system which supports the sort of thing you would like to have.


  • 1
    $\begingroup$ If I understand right, what you're saying is that the problems I sketched in the second paragraph are very much real. Nonetheless, there still could be a satisfactory answer, if there were a criteria which (like the one Evan gave) characterizes those groupoids which are equivalent to strict groupoids, but (unlike Evan's answer) is relatively trivial to understand. isSet has these properties, so even though you can't define sets internally to HoTT you can do something that's close enough (though the proof of "close enough" is necessarily external). $\endgroup$ – Noah Snyder Oct 8 '13 at 23:41
  • 1
    $\begingroup$ If you're trying to get strict groupoids up to equivalence, then of course there could be an internal definition. $\endgroup$ – Andrej Bauer Oct 9 '13 at 6:41
  • $\begingroup$ The links seem to be broken. $\endgroup$ – Giorgio Mossa Nov 5 '18 at 14:30

Strict $\infty$-groupoids are equivalent to crossed complexes, see paper available here, and the latter are often more convenient to handle, because of their analogies to chain complexes. The classifying space $BC$ of a crossed complex $C$ fibres over a $K(G,1)$ with fibre the classifying space of a chain complex, so up to homotopy a product of Eilenberg Mac Lane spaces. However crossed complexes are useful for discussing operations of the fundamental group, and in this respect have better realisation properties than chain complexes with operators, as JHC Whitehead observed in 1949.

The category of crossed complexes is monoidal closed so one can consider monoid objects in this category, and these contain some quadratic information.

However higher Whitehead products are well modelled by cat$^n$-groups ($n$-fold grouoids in the category of groups), and the equivalent category of crossed $n$-cubes of groups, see

Ellis, G. J. and Steiner, R., Higher-dimensional crossed modules and the homotopy groups of $(n+1)$-ads, J. Pure Appl. Algebra, 46 (1987) 117--136.

and the modelling of weak pointed homotopy $(n+1)$-types by cat$^n$-groups was shown by Loday (JPAA 1982).

It is possible that quadratic homotopy information is modelled by double crossed complexes, etc.

Edit: I would like to add that Thierry Coquand has a cubical set model for type theory available from here.

December 12, 2015

I should add that in the usual homotopy theory there is a theory of strict higher homotopy groupoids with useful applications, see the 2011 book Nonabelian Algebraic Topology, but a homotopically defined functor with values in strict cubical groupoids is defined there only on filtered spaces. There are several presentations (Paris (workshop on HTT), Galway, Aveiro, ...) on my preprint page giving more background to this. A naive question is whether filtered topoi or something analogous could be useful in HTT? Just as many useful spaces have some kind of dimensionwise structure, so this also may be true for types, especially if they are useful for describing mathematical structures, as would be my intuition, which is limited!

The presentation at CT2015 Aveiro is entitled "A philosophy of modelling and computing homotopy types", and shows briefly how you get some specific nonabelian computations.

  • $\begingroup$ I hope Mike Shulman will descend from the sky and answer whether this stuff, which is beyond me, is HoTT. $\endgroup$ – Andrej Bauer Oct 9 '13 at 13:28
  • $\begingroup$ @Andrej: It may be that the worlds of HOTT and Homotopy Theory are quite distinct, so I may have leapt in too quickly! But you never know. Your "infinite levels of structure" may be reflected in the use of filtered spaces in algebraic topology to construct strict $\infty$-groupoids. $\endgroup$ – Ronnie Brown Oct 9 '13 at 14:25
  • $\begingroup$ Your links do not seem to be working. $\endgroup$ – Baby Dragon Oct 9 '13 at 16:28
  • $\begingroup$ @Baby Dragon: Thanks! Now corrected. $\endgroup$ – Ronnie Brown Oct 9 '13 at 21:10
  • $\begingroup$ I am kind of doubtful that this perspective will be useful in HoTT, but you never know. One problem is that crossed complexes, as far as I can tell, will always have a set of objects, whereas that need not be true of an $\infty$-groupoid in HoTT, and probably not even a "strict" one. $\endgroup$ – Mike Shulman Oct 25 '13 at 5:08

Here's a partial answer to a related question. In classical stable homotopy theory, a spectrum is equivalent to a "strict" one (arising from a chain complex) if and only if it admits the structure of a module over $H\mathbb{Z}$, the Eilenberg-MacLane spectrum of the integers. This is potentially expressable in HoTT. (Specifically, we can currently define spectra and $H\mathbb{Z}$ and the smash product of spectra, but there are unresolved coherence questions involved in describing all the higher $E_\infty$ structure of a ring or module spectrum, similar to the problem of defining $(\infty,1)$-categories.)


I believe that an $\infty$-groupoid is strict if and only if all higher Whitehead products vanish. What this means more explicitly is that a space $X$ is (the homotopy type of) a strict $\infty$-groupoid if for every pair of natural numbers $m, n \geq 2$, every map that factorizes $S^{n + m - 1} \to S^n \vee S^m \to X$ is nullhomotopic. I don't know enough HoTT to say how to express this in that language, but it seems like it should be possible.

EDIT: As Charles points out in the comments, the condition that the Whitehead products vanish is necessary, but not sufficient for a space to have the homotopy type of a strict $\infty$-groupoid. However, I believe the result becomes true if we require that the so-called higher-order Whitehead products vanish as well (see this ancient paper). I'm not sure if this is equivalent to saying that every map that factorizes $S^{(\sum_{i = 1}^k n_i) - 1} \to \bigvee_{i = 1}^k S^{n_i} \to X$ is nullhomotopic; it may be more complicated than this.

  • $\begingroup$ Thanks, I think in principal I should be able to work out how to translate that into HoTT. However, I was really hoping that there'd be a definition of isStrict where I could prove that the Whitehead product for n=m=2 vanishes. Building that fact in feels like cheating. $\endgroup$ – Noah Snyder Oct 8 '13 at 20:38
  • 11
    $\begingroup$ I'm not sure I believe your criterion. Whitehead products always vanish in infinite loop spaces, but I wouldn't expect most infinite loop spaces to be modelled by strict $\infty$-groupoids. $\endgroup$ – Charles Rezk Oct 9 '13 at 1:50
  • 4
    $\begingroup$ Indeed, CSP gives an explicit counterexample at the nForum. $\endgroup$ – Noah Snyder Oct 9 '13 at 2:13
  • $\begingroup$ @NoahSnyder 's link is now nforum.ncatlab.org/discussion/4777/… $\endgroup$ – Charles Rezk Mar 3 '19 at 5:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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