[Nottingham Internship] Brunerie Type Theory, or how to concisely sum up the mess about $𝜔$-groupoids

4 minute read

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.

\[\newcommand{\rec}{\mathop{\rm rec}\nolimits} \newcommand{\ind}{\mathop{\rm ind}\nolimits} \newcommand{\inl}{\mathop{\rm inl}\nolimits} \newcommand{\inr}{\mathop{\rm inr}\nolimits} \newcommand{\Hom}{\mathop{\rm Hom}\nolimits} \newcommand{\Ty}{\mathop{\rm Ty}\nolimits} \newcommand{\Tm}{\mathop{\rm Tm}\nolimits} \newcommand{\op}{\mathop{\rm op}\nolimits} \newcommand{\Set}{\mathop{\rm Set}\nolimits} \newcommand{\1}{\mathbf{1}} \newcommand{\isContr}{\mathop{\rm isContr}\nolimits} \newcommand{\coh}{\mathop{\bf coh}\nolimits}\]

Brunerie Type Theory comes in

Brunerie type theory $𝔹$:

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

\[𝔹\\ \cfrac{}{\bullet ⊢ \star}\quad\text{(Base type)}\\ \\ \\ \\ \cfrac{Γ ⊢ x, y : A}{Γ \vdash x ≃ y}\quad\text{(Equality rule)}\\ \\ \\ \\ \cfrac{\isContr Γ \qquad Γ ⊢ A}{Γ \vdash \coh_A^Γ : A}\quad\text{(Coherence rule)}\]

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

a context $Γ$ is contractible iff:
  • $Γ = \bullet.\star$
  • or: $Γ ≝ Δ.(y:A).(p: y ≃ x)$ where $Δ$ is contractible and $x$ is a term of type $A$ in the context $Δ$

In other words:

\[\isContr (\bullet.\star) \\ \\ \\ \cfrac{\isContr Δ \qquad Δ ⊢ x: A}{\isContr Δ.(y:A).(p: x≃y)}\]

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 $ω$-groupoid.
  • if $x, y: \star$ the elements of $x ≃ y$ are the 1-arrows of $G_1(x, y)$
  • if $x, y: \star$ and $f, g: x ≃ y$, the elements of $f ≃ g$ are those of $G_1(f, g)$
  • and so on…

Now, with this analogy in mind, a context $Γ ≝ \bullet.(x \; y:\star).(f \; g : x ≃ y).(α : f ≃ g)$ will be depicted as

\[\begin{xy} \xymatrix{ x\ar@/^2pc/[rr]|f="ab1"\ar@/_2pc/[rr]|{g}="ab2"&& y } \ar@2{->}@/_/"ab1";"ab2"|\alpha \end{xy}\]

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

For instance:

  • the context $Γ ≝ \bullet.(x \; y \; z \; t:\star).(f : x ≃ y).(g : y ≃ z).(h : y ≃ t)$ is contractible

    \[\begin{xy} \xymatrix{ && && z \\ x\ar@/^/[rr]|f&& y\ar@/^/[rru]|g\ar@/_/[rrd]|h \\ && && t } \end{xy}\]

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

    \[\begin{xy} \xymatrix{ x\ar@/^/[rr]|f&& y, z\ar@/_/[rrd]|h \\ && && t } \end{xy}\]

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

    \[\begin{xy} \xymatrix{ x\ar@/^/[rr]|f&& y, z, t } \end{xy}\]

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

    \[\begin{xy} \xymatrix{ x, y, z, t } \end{xy}\]

  • but the context $Γ’ ≝ \bullet.(x \; y \; z \; t:\star).(f : x ≃ y).(g : y ≃ z).(h \; i : y ≃ t)$ is not contractible

    \[\begin{xy} \xymatrix{ && && z \\ x\ar@/^/[rr]|f&& y\ar@/^/[rru]|g\ar@/_/[rrd]|h\ar@/^/[rrd]|i \\ && && t } \end{xy}\]

    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 $Γ’’ ≝ \bullet.(x \; y \; z \; t:\star).(f : x ≃ y).(g : y ≃ z).(h \; i : y ≃ t).(α ≃ h \; i)$

    \[\begin{xy} \xymatrix{ && && z \\ x\ar@/^/[rr]|f&& y\ar@/^/[rru]|g\ar@/_2pc/[rrd]|h="h"\ar@/^2pc/[rrd]|i="i" \\ && && t } \ar@2{->}"h";"i"|\alpha \end{xy}\]

    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 $ω$-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≃y, \; g: y≃z, \; h: z≃t$ and $Γ_{x, y, z, t} ≝ \bullet.(x \; y \; z \; t : \star).(f : x ≃ y).(g : y ≃ z).(h : z ≃ t)$

\[\begin{xy} \xymatrix{ x\ar@/^/[rr]|f&& y\ar@/^/[rr]|g && z\ar@/^/[rr]|h && t } \end{xy}\]

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

As

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

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

$f *_1^1 g : x ≃ z$ can be defined in $Γ_{x, y, z, t}$ as $\coh_{x ≃ z}^{Γ_{x, y, z, t}}$

Similarly, $(f *_1^1 g) *_1^1 h$ can be defined as $\coh_{x ≃ t}^{Γ_{x, y, z, t}}$, and we proceed analogously for $g *_1^1 h$ and $f *_1^1 (g *_1^1 h)$.

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

\[𝛼^1(f, g, h) : (f *_1^1 g) *_1^1 h ≃ f *_1^1 (g *_1^1 h)\]

in $Γ_{x, y, z, t}$.

I think you’re beginning to get it: we use the contractibility of $Γ_{x, y, z, t}$ again (and the fact that $Γ_{x, y, z, t} ⊢ (f *_1^1 g) *_1^1 h ≃ f *_1^1 (g *_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: $\coh_{\star}^{\bullet.\star}, \; \coh_{\coh_{\star}^{\bullet.\star} ≃ x}^{\bullet.(x:\star)}, \; \ldots$

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 $ω$-groupoids.

Leave a comment