Now that you realize to what extent weak $𝜔$-groupoids are a mess, let’s have a look at a type theoretic and very concise way to define them, which is due to Guillaume Brunerie.

Brunerie Type Theory comes in

Brunerie type theory $𝔹$:

The Brunerie type theory $𝔹$ is given by these typing rules:

$$\begin{array}{c}𝔹\\ \frac{}{\bullet ⊢\star }\text{(Base type)}\\ \\ \\ \\ \frac{\Gamma ⊢x,y:A}{\Gamma ⊢x\simeq y}\text{(Equality rule)}\\ \\ \\ \\ \frac{\mathrm{isContr}\Gamma \Gamma ⊢A}{\Gamma ⊢{\mathbf{c}\mathbf{o}\mathbf{h}}_A^{\Gamma }:A}\text{(Coherence rule)}\end{array}$$

where $\mathrm{isContr}$ (which stands for “is contractible”) is inductively defined as follows:

a context $\Gamma$ is contractible iff:

• $\Gamma =\bullet .\star$
• or: $\Gamma \stackrel{\scriptscriptstyle\mathrm{def}}{=}\Delta .(y:A).(p:y\simeq x)$ where $\Delta$ is contractible and $x$ is a term of type $A$ in the context $\Delta$

In other words:

$$\begin{array}{c}\mathrm{isContr}(\bullet .\star )\\ \\ \\ \frac{\mathrm{isContr}\Delta \Delta ⊢x:A}{\mathrm{isContr}\Delta .(y:A).(p:x\simeq y)}\end{array}$$

The intuition behind is that

• the elements of the base type $\star$ correspond to the elements of the set $G_0$ of the underlying globular set of the weak $\omega$-groupoid.
• if $x,y:\star$ the elements of $x\simeq y$ are the 1-arrows of $G_1(x,y)$
• if $x,y:\star$ and $f,g:x\simeq y$, the elements of $f\simeq g$ are those of $G_1(f,g)$
• and so on…

Now, with this analogy in mind, a context $\Gamma \stackrel{\scriptscriptstyle\mathrm{def}}{=}\bullet .(xy:\star ).(fg:x\simeq y).(\alpha :f\simeq g)$ will be depicted as

A context is contractible if it can be “reduced to a point”, by contracting along the arrows.

For instance:

• the context $\Gamma \stackrel{\scriptscriptstyle\mathrm{def}}{=}\bullet .(xyzt:\star ).(f:x\simeq y).(g:y\simeq z).(h:y\simeq t)$ is contractible

  $$zxfyght$$

  Indeed, you can contract $z$ and $y$ along $g$:

  $$xfy,zht$$

  then $t$ and $y,z$ along $h$:

  $$xfy,z,t$$

  and finally $x$ and $y,z,t$ along $f$:

  $$x,y,z,t$$

• but the context ${\Gamma }^{\prime }\stackrel{\scriptscriptstyle\mathrm{def}}{=}\bullet .(xyzt:\star ).(f:x\simeq y).(g:y\simeq z).(hi:y\simeq t)$ is not contractible

  $$zxfyghit$$

  because there is a hole between $y$ and $t$ (thus, we can’t contract $y$ and $t$).

  But if the hole is filled by a 2-arrow, like in ${\Gamma }^{″}\stackrel{\scriptscriptstyle\mathrm{def}}{=}\bullet .(xyzt:\star ).(f:x\simeq y).(g:y\simeq z).(hi:y\simeq t).(\alpha \simeq hi)$

  $$zxfyghit\alpha$$

  then it becomes contractible ($i$ and $h$ can be contracted, following which we procceed similarly to the previous example).

What about the laws (that become part of the structure, in $\omega$-groupoids), such as the unit/associativity/interchange/coherence laws? They’re taken care of by Brunerie’s coherence rule, thanks to this notion of contractible contexts!

Let’s illustrate this with an example: for instance, the associativity law (along the $1$-arrows, to make things more simple (but the general case is quite similar)).

Let $x,y,z,t:\star ,f:x\simeq y,g:y\simeq z,h:z\simeq t$ and ${\Gamma }_{x,y,z,t}\stackrel{\scriptscriptstyle\mathrm{def}}{=}\bullet .(xyzt:\star ).(f:x\simeq y).(g:y\simeq z).(h:z\simeq t)$

First, how to define composition along the $1$-arrows?

As

• the context ${\Gamma }_{x,y,z,t}$ is contractible

• and ${\Gamma }_{x,y,z,t}⊢x\simeq z$ (since ${\Gamma }_{x,y,z,t}⊢x,z:\star$)

$f{\ast }_1^{1}g:x\simeq z$ can be defined in ${\Gamma }_{x,y,z,t}$ as ${\mathbf{c}\mathbf{o}\mathbf{h}}_{x\simeq z}^{{\Gamma }_{x,y,z,t}}$

Similarly, $(f{\ast }_1^{1}g){\ast }_1^{1}h$ can be defined as ${\mathbf{c}\mathbf{o}\mathbf{h}}_{x\simeq t}^{{\Gamma }_{x,y,z,t}}$, and we proceed analogously for $g{\ast }_1^{1}h$ and $f{\ast }_1^1(g{\ast }_1^{1}h)$.

From now on, our aim is to show that there exists a term

in ${\Gamma }_{x,y,z,t}$.

I think you’re beginning to get it: we use the contractibility of ${\Gamma }_{x,y,z,t}$ again (and the fact that ${\Gamma }_{x,y,z,t}⊢(f{\ast }_1^{1}g){\ast }_1^{1}h\simeq f{\ast }_1^1(g{\ast }_1^{1}h)$)!

NB: Hence, Brunerie’s coherence rule is very practical when it comes to expressing the unit/associativity/interchange/coherence laws!

But there’s a catch (kind of): therewith comes a whole bunch of redundant terms, such as: ${\mathbf{c}\mathbf{o}\mathbf{h}}_{\star }^{\bullet .\star },{\mathbf{c}\mathbf{o}\mathbf{h}}_{{\mathbf{c}\mathbf{o}\mathbf{h}}_{\star }^{\bullet .\star }\simeq x}^{\bullet .(x:\star )},\dots$

Right, so now we’re beginning to get the feeling as to why Brunerie’s type theory might be able to cover the notion of weak $\omega$-groupoids.