How do you define the strict infinity groupoids in Homotopy Type Theory?

Question

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?

Answer 1

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.

Answer 2

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.

References:

• V. Voevodsky: A simple type system with two identity types, notes.
• V. Voevodsky:A type system with two kinds of identity types, talk slides.

Answer 3

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.

Answer 4

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.)

Answer 5

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.