Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Invertible cells in $ω$-categories

Thibaut Benjamin, Ioannis Markakis

TL;DR

This work develops a syntactic, computad-based approach to invertibility in weak $\omega$-categories. It proves that invertible cells are closed under all $\omega$-category operations by exploiting a coinductive definability of invertibility, a rich toolkit of meta-operations (including suspension, opposites, functorialisation and chain reduction), and explicit constructions (fillers, associators, unitors, telescopes) to build inverses and witnesses. A key contribution is a finite, constructive criterion for invertibility in finite-dimensional computads, along with an algorithm that computes the inverse and cancellation data. The results are implemented in CaTT, enabling automatic computation of inverses and witnesses, and demonstrated via the Eckmann–Hilton cell, underscoring the practical potential of syntactic methods in higher category theory.

Abstract

We study coinductive invertibility of cells in weak $ω$-categories. We use the inductive presentation of weak $ω$-categories via an adjunction with the category of computads, and show that invertible cells are closed under all operations of $ω$-categories. Moreover, we give a simple criterion for invertibility in computads, together with an algorithm computing the data witnessing the invertibility, including the inverse, and the cancellation data.

Invertible cells in $ω$-categories

TL;DR

This work develops a syntactic, computad-based approach to invertibility in weak -categories. It proves that invertible cells are closed under all -category operations by exploiting a coinductive definability of invertibility, a rich toolkit of meta-operations (including suspension, opposites, functorialisation and chain reduction), and explicit constructions (fillers, associators, unitors, telescopes) to build inverses and witnesses. A key contribution is a finite, constructive criterion for invertibility in finite-dimensional computads, along with an algorithm that computes the inverse and cancellation data. The results are implemented in CaTT, enabling automatic computation of inverses and witnesses, and demonstrated via the Eckmann–Hilton cell, underscoring the practical potential of syntactic methods in higher category theory.

Abstract

We study coinductive invertibility of cells in weak -categories. We use the inductive presentation of weak -categories via an adjunction with the category of computads, and show that invertible cells are closed under all operations of -categories. Moreover, we give a simple criterion for invertibility in computads, together with an algorithm computing the data witnessing the invertibility, including the inverse, and the cancellation data.
Paper Structure (24 sections, 18 theorems, 132 equations, 1 figure)

This paper contains 24 sections, 18 theorems, 132 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Globular pasting diagrams
  3. Globular sets
  4. Batanin trees and their positions
  5. Operations on pasting diagrams
  6. Weak ω-categories
  7. Computads
  8. ω-categories
  9. Suspensions and opposites
  10. Invertible and equivalent cells
  11. Constructions in weak ω-categories
  12. Unbiased unitors
  13. Filler cells
  14. Functorialisation of coherences
  15. Chain reduction
  16. ...and 9 more sections

Key Result

Proposition 9

For every $k\in \mathbb{N}$ and every pair of Batanin trees $B$ and $B'$ sharing a common $k$-boundary, there exists a pushout square of the form \begin{tikzcd} \Pos{\partial_k B} & \Pos{\partial_k B'} & \Pos{B'} \\ \Pos{B} && \Pos{\graft{k}{B}{B'}} \arrow["{\tgtps[k]{B}}"', from=1-1, to

Figures (1)

  • Figure 1: Mechanisation of the cancellation data $\mathop{\mathrm{u}}\nolimits$ of the Eckmann-Hilton cell.

Theorems & Definitions (53)

  • Definition 1
  • Definition 2
  • Definition 3
  • Example 4
  • Example 5
  • Definition 6
  • Remark 7
  • Definition 8
  • Proposition 9
  • proof
  • ...and 43 more