Context
Given a finitary monad $T:\operatorname{gSet}_n\to\operatorname{gSet}_n$ we can define categories $\operatorname{Comp}_k^T$ of $k$-computads for $T$, for any $k=0,\cdots,n+1$. This is nicely explained in Schommer-Pries' thesis, for example and the original source is this paper of Batanin. Essentially a $k$-computad $C$ is defined inductively as a tuple $(C_k,C_{\leq k -1},s,t)$ where $C_k$ is a set (the set of $k$-cells), $C_{\leq k-1}$ is a $(k-1)$-computad and $s,t$ are maps $C_k\to [F_{k-1}(C_{\leq k-1})]_{k-1}$ where $F_{k-1}$ is the functor that constructs the $T$-algebra generated by a $(k-1)$-computad. These are required to satisfy the usual globularity conditions $ss=st$ and $ts=tt$. Then one completes the induction by defining $F_k$ by a certain pushout diagram in $\operatorname{Alg_T}$ (using the fact that $\operatorname{Alg_T}$ is cocomplete, because $T$ is finitary).
Questions
- Is the category $\operatorname{Comp}_k^T$ always cocomplete?
- Does the functor $\operatorname{Comp}_k^T\to\operatorname{Set}$ that takes a computad to its set of $i$-cells for some $i\leq k$ preserve colimits?
- Is there a reference for these facts?
If there is no reference, then
- Is the sketch of proof below correct, or am I missing something?
Sketch of proof of 1. and 2.
One constructs the colimit of some diagram $C(i)$ of $k$-computads by induction on $k$: one constructs a $k$-computad whose set of $k$-cells is the colimit of the diagram on $k$-cells and whose underlying $(k-1)$-computad is the colimit of the diagram of underlying $(k-1)$-computads. Source and target maps $\operatorname{colim}_i C(i)_k\to [F_{k-1}(\operatorname{colim}_i C(i)_{\leq k-1})]_{k-1}$ can be defined by the composite $$C(i)_k\to [F_{k-1}(C(i)_{\leq k-1})]_{k-1}\to\operatorname{colim}_i [F_{k-1}(C(i)_{\leq k-1})]_{k-1}\to[\operatorname{colim}_iF_{k-1}(C(i)_{\leq k-1})]_{k-1}=[F_{k-1}(\operatorname{colim}_i C(i)_{\leq k-1})]_{k-1}$$ where the equality comes from the fact that $F_{k-1}$ is left adjoint and the final arrow is induced by the maps $[F_{k-1}(C(i)_{\leq k-1})]_{k-1}\to[\operatorname{colim}_iF_{k-1}(C(i)_{\leq k-1})]_{k-1}$ which are the maps of underlying $(k-1)$-morphisms associated to the canonical maps of $T$-algebras $F_{k-1}(C(i)_{\leq k-1})\to\operatorname{colim}_iF_{k-1}(C(i)_{\leq k-1})$.
Now one needs to check that $s,t$ satisfy globularity and that the construction has the right universal property. This also seems completely straightforward.
What I have found in the literature
In the above cited paper of Batanin, it is proved that when the monad is truncable and preserves finite pullbacks, the category $\operatorname{Comp}_n^T$ is an elementary topos, so it particular has finite colimits. It is also proved that if additionally $T$ preserves wide pullbacks and the unit is cocartesian then $\operatorname{Comp}_n^T$ is a presheaf topos, so in particular is cocomplete. This appears as Theorem 4.1.
I am hoping, however, that if one only needs cocompleteness then the hypotheses are not necessary and there is the above direct proof.
Best Answer
The answer to $1$ and $2$ are both yes. I don't know if this appears in the literature. The argument you give seems reasonable - I don't completely follow your notation but the general idea is that in the "inductive" definition of computads, you can show that colimits of "k-computads" are computed by taking the colimit of the (k-1)-computads and the sets of k-cells separately, which seems to be exactly what you are saying. Colimits of general computads are then computed by taking the colimit of their "underlying k-computads" for all k.
I would consider this as a folklore results in the area, and I wouldn't be surprised if it is written somewhere, at least for the special case of the strict $\infty$-category monads, but I couldn't find a reference to give you.
Note however that the results of Batanin you quote is unfortunately false - the category of computads for the free strict $\infty$-category (which satisfies all the assumption of Batamin's theorem) is not a topos. In fact it is not cartesian closed (or here).
A latter paper of Batanin gives a finer criterion for such categories of computads to indeed be presheaf categories which I think* is correct. This second paper applies for example to the computads for Batanin's definition of weak $\infty$-categories.
*: To be clear, I have to admit I have never been able to fully understand the argument given by Batanin in this second paper, and the paper has never been published, so I can't tell if the proof given there is correct (though I have no reasons to doubt it is). But, this being said I have very good reason to believe the result itself is definitely correct due to my own work on the topic which involves similar assumptions.