Computads for weak \(\omega \)-categories as an inductive type (Q6562849)

We may generate a free \(\omega\)-category from a computad, yielding an adjunction.\N\[\N\mathsf{Comp} \begin{array} [c]{c} \longrightarrow\\\N\bot\\\N\longleftarrow \end{array} \omega\mathsf{Cat}\N\]\NThe study of 2-computads was initiated by \textit{R. Street} [J. Pure Appl. Algebra 8, 149--181 (1976; Zbl 0335.18005)], and the theory of \(n\)-computads is now well-established, with key contributions by \textit{M. A. Batanin} [Contemp. Math. 230, 37--57 (1998; Zbl 0932.18004)], \textit{R. Garner} [Adv. Math. 224, No. 6, 2269--2311 (2010; Zbl 1205.18004)] and others. The category \ of weak \(\omega\)-categories and strict \(\omega\)-functors is defined as the category of algebras for a finitary monad on globular sets, while \(n\)-computads are defined inductively on \(n\), via a colimit construction in \(\omega\mathsf{Cat}\)\ involving an infinite sequence of pushouts [\textit{J. Adamek} and \textit{V. Koubek}, J. Algebra 66, 226--250 (1980; Zbl 0446.18003), \S I.5].\N\NThis paper shows that the quotient set does in fact admit a direct desccription in each dimension as a family of inductive sets, which yields an elementary and fully explicit definition of computads for weak globular \(\omega\)-categories. It is shown that this definition reproduces the universal cofibrant replacement of \textit{R. Garner} [Adv. Math. 224, No. 6, 2269--2311 (2010; Zbl 1205.18004)], demonstrating that every \(\omega\)-category is equivalent to one which is free on a computad. The authors observe that the category of computads with structure-preserving maps is a presheaf topos. It is shown that the definition of \(\omega\)-category arising from this work agrees precisely with the notion of weak \(\omega \)-category described by \textit{M. A. Batanin} [Adv. Math. 136, No. 1, 39--103 (1998; Zbl 0912.18006)] and \textit{T. Leinster} [Higher operads, higher categories. Cambridge: Cambridge University Press (2004; Zbl 1160.18001)].\N\NThe authors' approach yields the category of computads \(\mathsf{Comp}\)\ as the primary object of study constructed directly without passing via any pre-existing definition of \(\omega\)-category. They then exhibit an adjunction between \(\mathsf{Comp}\)\ and the category \(\mathsf{Glob}\)\ of globular sets, definilng \(\omega\mathsf{Cat}\)\ as the category of algebras for the monad yielded naturally on \(\mathsf{Glob}\). The resulting situation is depicted by the folloiwng diagram.\N\[\N\begin{array} [c]{ccc} \mathsf{Comp} & \longrightarrow & \omega\mathsf{Cat}\\\N\underset{\nwarrow}{\underset{\top}{\searrow}} & & \underset{\nearrow }{\underset{\top}{\swarrow}}\\\N& \mathsf{Glob} & \end{array}\N\]