Computads for weak $\omega$-categories as an inductive type

Abstract

We give a new description of computads for weak globular $\omega$-categories by giving an explicit inductive definition of the free words. This yields a new understanding of computads, and allows a new definition of $\omega$-category that avoids the technology of globular operads. Our framework permits direct proofs of important results via structural induction, and we use this to give new proofs that every $\omega$-category is equivalent to a free one, and that the category of computads with generator-preserving maps is a presheaf topos, giving a direct description of the index category. We prove that our resulting definition of $\omega$-category agrees with that of Batanin and Leinster and that the induced notion of cofibrant replacement for $\omega$-categories coincides with that of Garner.

References in corpus (2)

• Towards 3-Dimensional Rewriting Theory
• A direct proof that the category of 3-computads is not cartesian closed

Cited by in corpus (1)

• CaTT contexts are finite computads