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

TL;DR

This paper introduces a new inductive approach to defining computads for weak globular -categories, simplifying the understanding and proofs of key properties without relying on globular operads.

Contribution

It provides an explicit inductive definition of free words for computads, enabling direct structural proofs and aligning with existing -category frameworks.

Findings

Every -category is equivalent to a free one.

The category of computads forms a presheaf topos.

The new definition agrees with established -category theories.

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.