# [Nottingham Internship] weak $𝜔$-groupoids: the DIY way

Let’s take a look at what $G_1$ and $G_2$ look like in Type Theory, if $G ≝ \bigsqcup\limits_{n≥0} G_n$ is a weak $𝜔$-groupoid: the laws of $G_n$ now become elements of $G_{n+1}$, which themselves induce new coherence laws at level $G_{n+2}$, which themselves… and so on.

### $G_1$

• Identity:

${\rm id}^1 (\_ ) : \prod\limits_{a: G_0} G_1(a, a)$
• Inverse:

${\rm inv}^1 (\_ , \_ ) : \prod\limits_{a, b: G_0} G_1(a, b) ⟶ G_1(b, a)$
• Composition:

$*^1_1 (\_ , \_ , \_ ) : \prod\limits_{a, b, c: G_0} G_1(a, b) × G_1(b, c) ⟶ G_1(a, c)$

### $G_2$

• Associativity along the $1$-arrows:

$𝛼^1 (\_ , \_ , \_ ) : \prod\limits_{f, g, h: G_1} G_2((f *_1^1 g) *_1^1 h, \; f *_1^1 (g *_1^1 h))$
• Left identity law:

$𝜆^1 (\_ ) : \prod\limits_{f: G_1} G_2(({\rm id}^1_{s f} *_1^1 f), \; f)$
• Right identity law:

$𝜌^1 (\_ ) : \prod\limits_{f: G_1} G_2((f *_1^1 {\rm id}^1_{t f}), \; f)$
• Left inverse law:
$l^1 (\_ ) : \prod\limits_{f: G_1} G_2(({\rm inv}^1_{sf, tf}(f) *_1^1 f), \; {\rm id}^1_{t f})$
• Right inverse law:
$r^1 (\_ ) : \prod\limits_{f: G_1} G_2((f *_1^1 {\rm inv}^1_{sf, tf}(f)), \; {\rm id}^1_{s f})$
• Identity:

${\rm id}^2 (\_ ) : \prod\limits_{f: G_1} G_2(f, f)$
• Inverse:

${\rm inv}^2 (\_ , \_ ) : \prod\limits_{f, g: G_1} G_2(f, g) ⟶ G_2(g, f)$
• Horizontal Composition (along the $1$-arrows):

$*^2_1: \prod\limits_{x, x', x'': G_0}\prod\limits_{f, f': G_1(x, x'), g, g': G_1(x', x'')} G_2(f, f') × G_2(g, g') ⟶ G_2(f *_1^1 g, \, f' *_1^1 g') \\ \begin{xy} \xymatrix{ x\ar@/^2pc/[rr]|f="ab1"\ar@/_2pc/[rr]|{f'}="ab2"&& x'\ar@/^2pc/[rr]|g="bc1"\ar@/_2pc/[rr]|{g'}="bc2" && x'' } \ar@2{->}@/_/"ab1";"ab2"|\alpha \ar@2{->}@/_/"bc1";"bc2"|{\alpha'} \end{xy} \\ \cfrac{𝛼:G_1(x, x')\\ 𝛼': G_1(x', x'')}{𝛼 *_1^2 𝛼': G_1(x, x'')}$
• Vertical Composition (along the $2$-arrows):

$*^2_2: \prod\limits_{x, x': G_0}\prod\limits_{f, f', f'': G_1(x, x')} G_2(f, f') × G_2(f', f'') ⟶ G_2(f, f'') \\ \\ \begin{xy} \xymatrix{ x\ar@/^3pc/[rr]|f="ab1"\ar[rr]|{f'}="ab2"\ar@/_3pc/[rr]|{f''}="ab3"&& x' } \ar@2{->}"ab1";"ab2"|\alpha \ar@2{->}"ab2";"ab3"|{\alpha'} \end{xy} \\ \\ \cfrac{𝛼:G_2(f, f')\\ 𝛼': G_2(f', f'')}{𝛼 *_2^2 𝛼': G_2(f, f'')}$

### $G_3$, and so on

At level $3$, in addition to that, we’ve got to take into account

• interchange law:

$\begin{xy} \xymatrix{ x\ar@/^3pc/[rr]|f="ab1"\ar[rr]|{f'}="ab2"\ar@/_3pc/[rr]|{f''}="ab3"&& x'\ar@/^3pc/[rr]|g="bc1"\ar[rr]|{g'}="bc2"\ar@/_3pc/[rr]|{g''}="bc3" && x'' \ar@{~>}@/_1pc/[rr]|{\text{horizontal}} && x\ar@/^3pc/[rr]|{f *_1^1 g}="ac1"\ar[rr]|{f' *_1^1 g'}="ac2"\ar@/_3pc/[rr]|{f'' *_1^1 g''}="ac3"&& x' \\ && \ar@{~>}[dd]|{\text{vertical}} && && && \ar@{~>}[dd]|{\text{vertical}} \\ && && && && \\ && && && && \\ x\ar@/^2pc/[rr]|f="a'b'1"\ar@/_2pc/[rr]|{f''}="a'b'2"&& x'\ar@/^2pc/[rr]|g="b'c'1"\ar@/_2pc/[rr]|{g''}="b'c'2" && x'' \ar@{~>}@/^1pc/[rr]|{\text{horizontal}}&& x\ar@/^2pc/[rrrr]|{f *_1^1 g}="a'c'1"\ar@/_2pc/[rrrr]|{f'' *_1^1 g''}="a'c'2"&&&& x'' } \ar@2{->}"ab1";"ab2"|\alpha \ar@2{->}"ab2";"ab3"|{\alpha'} \ar@2{->}"bc1";"bc2"|\beta \ar@2{->}"bc2";"bc3"|{\beta'} \ar@2{->}"ac1";"ac2"|{\alpha *_1^2 \beta} \ar@2{->}"ac2";"ac3"|{\alpha' *_1^2 \beta'} \ar@2{->}"a'b'1";"a'b'2"|{\alpha *_2^2 \alpha'} \ar@2{->}"b'c'1";"b'c'2"|{\beta *_2^2 \beta'} \ar@2{->}"a'c'1";"a'c'2"|{(\alpha *_1^2 \beta) *_2^2 (\alpha' *_1^2 \beta') = (\alpha *_2^2 \alpha') *_1^2 (\beta *_2^2 \beta')} \end{xy}$
• the different compositions $*_1^3, *_2^3, *_3^3$

• new coherence laws between the previous ones

Tags:

Updated: