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

2 minute read

Handmade partial construction

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

Leave a comment