Proof. We describe universal expressions before evaluating them in a model. For each \(k>i\), let \((g,a)\) be the generic pair of \(i\)-composable \(k\)-cells on \(d_k\amalg_{d_i}d_k\). Initially put \[U_{i+1}^k(g,a)=w_i(g)*_i(g*_i a).\] We inductively construct \(U_h^k\) for \(k\ge h>i\) with the following two properties: its faces below \(h\) equal those of \(a\), and its \(l\)-faces for \(h\le l<k\) are \(U_h^l\) evaluated on the corresponding \(l\)-faces of \((g,a)\). These statements hold for \(h=i+1\) by the exact face equations just given. In particular \(U_h^h(g,a)\) and \(a\) are parallel as operations on the generic pair of \(h\)-globes. Choose admissible operations \[c_h(g,a):a\longrightarrow U_h^h(g,a),\qquad d_h(g,a):U_h^h(g,a)\longrightarrow a.\] They have output dimension \(h+1\) on an arity of height \(h\). For \(k>h\), define \[ \begin{split} U_{h+1}^k(g,a)={}& e_{h+1}^k d_h(t_hg,t_ha)\ *_h\bigl( U_h^k(g,a)\ *_h e_{h+1}^k c_h(s_hg,s_ha)\bigr). \end{split} \tag{3}\] The two compositions are defined because the old \(h\)-faces are \(U_h^h\) on the indicated face inputs. Their new \(h\)-faces are exactly \(s_ha,t_ha\), and lower faces retain their required values. Faces above \(h\) obey the same formula in their own dimension, by the composition and unit face equations. This proves both inductive properties. Notice that parallelism for \(c_h,d_h\) is an identity in their arity, and does not result from a special equality in the model under consideration.

Now prescribe the input boundary of an \(r\)-cell \(\alpha\), without assuming that such a cell exists, and let \(\beta\) have the induced boundary of \(\gamma*_i\alpha\). Begin with \(z=w_i(\gamma)*_i\beta\). For \(h=i+1,\ldots,r-1\), replace \(z\) by the right side of Equation (3), with \(k=r\), \(U_h^r(g,a)\) replaced by \(z\), and the correction factors evaluated at \((s_h\gamma,s_h\alpha)\) and \((t_h\gamma,t_h\alpha)\). These faces of \(\alpha\) belong to the prescribed boundary. At every stage the proper faces of \(z\) obey the universal formulas already proved, because \(\beta\) has the prescribed output boundary. The construction therefore finishes with an \(r\)-cell \(K_\gamma(\beta)\) having exactly the desired input boundary.

All correction factors depend only on \(\gamma\) and that boundary. Write \(L_\gamma\) for left multiplication by \(\gamma\) on homotopy classes. Thus \(K_\gamma\) is a composite of multiplication maps by fixed cells and induces a map of homotopy sets. On an actual input \(\beta=\gamma*_i\alpha\), it equals \(U_r^r(\gamma,\alpha)\). The latter is parallel to \(\alpha\) on the generic pair of \(r\)-globes, so an admissible \((r+1)\)-filler shows that \(K_\gamma L_\gamma=\mathrm{id}\) on classes.

The same construction with left and right interchanged gives a left inverse for every right multiplication. Consequently all left and right multiplication maps are injective. Each factor of \(K_\gamma\) is one of these now-known injective maps, so \(K_\gamma\) is injective as well. Applying this injectivity to \(K_\gamma L_\gamma K_\gamma=K_\gamma\) gives \(L_\gamma K_\gamma=\mathrm{id}\). This proves bijectivity without a nonemptiness assumption on the input set. ◻

Proof. The last assertion is composition in the groupoid above. When \(r=1\), the first assertion is the definition and change of vertex is conjugation in the fundamental groupoid. For \(r\ge2\), put \(x=s_0u\), \(a=e_0^{r-1}(x)\) and \(w=u*_0a\), and abbreviate \(e(u)\) to \(1_u\). Lemma 3 gives a span of bijections \[\pi_r(X;u,u) \xrightarrow{\ [\alpha]\mapsto[\alpha*_0 1_a]\ } \pi_r(X;w,w) \xleftarrow{\ [\beta]\mapsto[1_u*_0\beta]\ } \pi_r(X;a,a).\] For the target vertex \(y=t_0u\), use \(b=e_0^{r-1}(y)\) and \(w'=b*_0u\) instead: the maps are \([\alpha]\mapsto[1_b*_0\alpha]\) and \([\beta]\mapsto[\beta*_0 1_u]\). Finally, for an arrow \(p:x\to y\), apply these two comparisons to \(u=e_1^{r-1}(p)\). Naturality follows from the fixed choices of operations; inverses of the resulting bijections are natural too. Only set bijections are needed here. ◻

Proof. Suppose (1) holds. Lemma 4 shows that \(f\) is bijective on every endomorphism homotopy set. We prove (2) by induction on \(r\). First address existence of a class: if a \(1\)-cell joins \(fu\) to \(fv\), injectivity on \(\pi_0\) gives a cell \(u\to v\). If \(r>1\) and a target \(r\)-cell joins \(fu\) to \(fv\), then \(fu,fv\) represent the same class in the appropriate \((r-1)\)-dimensional homotopy set. Injectivity already proved in dimension \(r-1\) gives a source \(r\)-cell \(u\to v\). Thus a nonempty target homotopy set has a nonempty source homotopy set. Choose a source joining cell; composition with it and its image identifies the map on these homotopy sets with the map on endomorphism sets. The latter is bijective. If the target set is empty, the source is empty as well, so the assertion also holds in that case.

Condition (2) immediately gives (3), using surjectivity on \(\pi_0\) when \(r=0\). Conversely (3) gives surjectivity on \(\pi_0\) and on every homotopy set at a source boundary. If parallel source \(r\)-cells have homotopic images, apply (3) in dimension \(r+1\) to their exact boundary and the target joining cell. This produces a source joining cell. For \(r=0\) it proves injectivity on \(\pi_0\), and for \(r\ge1\) it proves injectivity on the indicated homotopy sets. Hence (2) follows, and its based instances give (1). ◻

Proof. For two-out-of-three, use the induced maps of components and based groups. In the case where \(f\) and \(gf\) are weak equivalences, a vertex of the intermediate model is joined to some \(f(x)\), by surjectivity of \(\pi_0(f)\). Lemma 4 transfers bijectivity of the homomorphism induced by \(g\) at \(f(x)\) to that vertex. The other two cases follow directly by cancellation of bijections. Retract closure follows from Proposition 5(3), even for a retract of underlying globular arrows: apply its disk and homotopy witnesses in the larger arrow and retract them.

For a filtered colimit of weak equivalences, the prescribed boundary, target disk, and their finitely many matching equations in Proposition 5(3) all occur together at some stage. Apply the test there and map its two witnesses to the colimit. Finally, transfinite induction handles a transfinite composite: use composition at successor stages and, at a limit, apply filtered-colimit closure to the arrows from the constant initial stage to the preceding stages. No injectivity of the transition maps is required. ◻

Proof. For a square against \(I_j\), Proposition 5 provides an approximate \(j\)-cell lift \(x\) and a target \((j+1)\)-cell \(H:fx\to y\). Lifting \(H\) against \(J_j:D_j\to D_{j+1}\) with prescribed source \(x\) gives a \((j+1)\)-cell whose target is a strict lift of \(y\) with the specified boundary. This also proves the assertion for \(j=0\).

An \(I\)-injective map satisfies the test strictly, using the unit on the target disk as its homotopy, so it belongs to \(\mathcal W\). Each \(J_j\) is the composite of two boundary attachments: first adjoin the parallel target \(j\)-cell using \(I_j\), then the joining \((j+1)\)-cell using \(I_{j+1}\). Thus \(I\)-injectivity implies \(J\)-injectivity, and the first paragraph proves the reverse inclusion in the displayed equality. Finally a \(J_j\)-lifting problem for \(X\to1\) is solved by the unit on its prescribed source cell. ◻

Proof. On underlying globular sets, retain the cells and face maps of \(X\) through dimension \(q\). In successive dimensions \(j>q\), put one \(j\)-cell over each parallel pair of \((j-1)\)-cells. Denote the resulting globular set by \(Z\). There is a canonical globular map \(\eta:X\to Z\), equal to the identity through \(q\).

To interpret the theory on \(Z\), follow the given free cellular presentation of \(\mathcal C\) in its original order. Maintain that \(\eta\) respects the part of the theory already interpreted. Suppose a newly adjoined generating operation has output dimension \(j\) and arity \(S\). Its two prescribed faces are operations of the earlier theory.

If \(j\leq q\), the generating arity bound \(\dim(S)\leq j\) in Definition 2 makes the tuple sets on \(S\) in \(X\) and \(Z\) identical. Use the original interpretation in \(X\). Its prescribed face equations hold in \(Z\): the tuple comes from \(X\), and \(\eta\) already respects both earlier face operations. It also respects the new operation, since it is the identity in dimension \(j\).

If \(j>q\), the earlier interpretation gives a parallel boundary in \(Z\), and the new operation is its unique filler. The image under \(\eta\) of the operation in \(X\) has that boundary, so uniqueness again shows compatibility with \(\eta\). At a limit stage take the union of the preceding interpretations. Freeness of the presentation now gives a model structure on \(Z\). This argument places no bound on the arities of composite face operations and does not reorder generators by dimension.

For a \(q\)-coskeletal model \(Y\), a model map \(f:X\to Y\) has a unique globular factorization through \(\eta\): use \(f\) through dimension \(q\) and unique fillers thereafter. This factorization is a model map. For a generator of output at most \(q\), every tuple comes from \(X\); for a higher generator, preservation follows from uniqueness in \(Y\). This proves the adjunction. Starting with \(X\in\mathcal A_q\) and performing the construction at \(k<q\) proves the remaining statements by the same universal property. ◻

Proof. The reflection of \(I_j\) into \(\mathcal A_k\) is an isomorphism when \(j>k\): every \(k\)-coskeletal model has a unique filler of every \(j\)-boundary. Reflect a pushout, a coproduct of attachments, or a transfinite composite of such maps. Colimit preservation makes its reflection an isomorphism. Since both reflection units preserve the cells through \(k\), the original map is bijective on those cells. Within \(\mathcal A_q\), use the further reflection to \(\mathcal A_k\). Finally, \(J_j\) is the composite of an \(I_j\) attachment, adjoining its new target \(j\)-cell, and an \(I_{j+1}\) attachment, adjoining the comparison cell. ◻

Proof. First, every shape \(S\) can be built from \(v(S)\) by finitely many source inclusions \(d_j\to d_{j+1}\) with \(j\geq0\). This is induction on the recursive description. If \(S\) is a vertex there is nothing to attach. Otherwise, for \(S=[S_1,\ldots,S_p]\), first build the outer vertex string by source inclusions in dimension zero, using in its \(i\)th slot the edge corresponding to \(v(S_i)\). Then build each \(S_i\) from \(v(S_i)\) by the induction hypothesis and suspend its attachments into that slot. Under this suspension an elementary pair of dimensions \((j,j+1)\) becomes one of dimensions \((j+1,j+2)\), with exactly the same source-attachment description. This follows directly from the face maps: the two added cells acquire the fixed outer poles, and their other faces are the suspended old faces.

The height and lower-cell claims for \(T_m\) now follow directly from Equation (4). For the attachment claim when \(m=0\), rebuild each \(S_i\) from \(v(S_i)\) as above. All these attachments are suspended once, so their indices are at least one. For \(m\geq1\), the induction hypothesis for \(T_{m-1}(S_i)\to S_i\) uses indices \(j>m-1\); suspending gives indices \(j+1>m\). Apply this construction in every slot. There are finitely many slots and attachments because \(S\) is finite. ◻

Proof. Let \(a,b\) be parallel \(m\)-cells of \(F(S)\), where \(m\geq0\) and in dimension zero there is no parallelism condition. By Lemmas 11 and 10, the map \(F(T_m(S))\to F(S)\) is bijective on every cell set through \(m\). Hence \(a,b\) have unique lifts \(a',b'\) there, and the lifts are parallel: their lower faces agree by the same injectivity.

The free model on a globular-sum shape is represented by that object of \(\mathcal C\). Thus \(a',b'\) are a parallel pair of theory arrows with domain the \(m\)-globe and codomain \(T_m(S)\). Since \(\dim(T_m(S))\leq m+1\), this pair is admissible for a filler of dimension \(m+1\). Contractibility of \(\mathcal C\) supplies such a filler. Its image joins \(a\) to \(b\) in \(F(S)\). The model is nonempty because \(S\) has a vertex, so the contractibility criterion of Proposition 5 applies. No assertion about weak equivalences of elementary attachments was used here.

For \(F_q(S)\), a parallel pair of \(m\)-cells with \(m<q\) lifts to \(F(S)\) by Lemma 9; the filler just constructed is preserved through dimension \(m+1\leq q\). If \(m\geq q\), the required filler has dimension \(m+1>q\) and exists uniquely. The vertex is retained, so \(F_q(S)\) is also contractible. ◻

Proof. Let \(i:X\to Y\) be a pushout of \(J_q\). It has a retraction \(r:Y\to X\), obtained by sending the new \(q\)-cell to the attaching cell and its comparison to a unit. For \(q>0\), Lemma 10 shows that \(i\) is bijective on cells through dimension \(q-1\).

Check the exact-boundary criterion of Proposition 5 in dimension \(d\). If \(d<q\), the given \(d\)-cell of \(Y\) comes from a unique \(d\)-cell of \(X\), whose boundary is the prescribed one by injectivity on lower cells. Its image is the given cell, so its unit supplies the homotopy. If \(d=q\), apply \(r\) to the given cell. Its boundary is the prescribed boundary because \(ri=\mathrm{id}_X\), and its image is parallel to the given cell. These two \(q\)-cells have a unique joining \((q+1)\)-cell. If \(d>q\), the prescribed source boundary has a unique filler in \(X\), whose image is the given filler in \(Y\). This proves the criterion in every dimension. For \(q=0\), the first case is absent; the same retraction and unique-arrow argument proves the dimension-zero case directly. ◻

Proof. Apply the ordinary small-object construction with the upper \(J_j\) to factor \(i\) as \[U\xrightarrow{\,a\,}Z\xrightarrow{\,p\,}V,\] where \(a\) is upper \(J\)-cellular and \(p\) lifts against every upper \(J_j\). The preceding induction hypotheses imply \(a\in\mathcal W\), so \(p\in\mathcal W\) by two-out-of-three. By Lemma 8, \(p\) lifts against every upper \(I_j\): the approximate lift of a \(j\)-cell is corrected by lifting its \((j+1)\)-dimensional homotopy against \(J_j\). In particular the lowest index required is \(J_{n+1}\), which is already available.

Since \(i\) is upper \(I\)-cellular, there is a map \(s:V\to Z\) with \(si=a\) and \(ps=\mathrm{id}_V\). Thus, in the category under \(U\), the map \(i\) is a retract of \(a\). Each individual \(J_j\) attachment admits a unit retraction. A transfinite composite of such attachments also retracts to its initial object: choose the maps back recursively at successor stages, and use their compatible colimit map at a limit stage. Let \(t:Z\to U\) be the resulting retraction of \(a\). Then \(ts\) is a retraction of \(i\).

Push the retract diagram out along \(U\to U'\). The pushout of \(i\) is a retract of the pushout of \(a\), and the latter is upper \(J\)-cellular with cellular source \(U'\). It is therefore in \(\mathcal W\) by the induction hypotheses. Retract closure proves the claim. ◻

Proof. In each depth-\(n\) slot, order its tree vertices in any way and replace the tree by the forward linear string on those same labeled vertices. A singleton remains a singleton. The resulting globular set \(K^{\mathrm{lin}}\) is a globular-sum shape, and its cells through dimension \(n\) are canonically the same as those of \(K\); Figure [fig:tree-string] illustrates one slot. Reordering within a slot leaves unchanged any outer poles and every earlier concatenation or suspension. Put \[A=F_q(K),\qquad L=F_q(K^{\mathrm{lin}}).\] The model \(L\) is contractible by Proposition 12.

There are model maps \[f:A\longrightarrow L,\qquad g:L\longrightarrow A\] fixing the generating cells through dimension \(n\). To define \(f\), send each tree edge to a composite along the path between its endpoints in the corresponding line, using inversion for any backward traversal. Define \(g\) using paths in the tree. All compositions are at level \(n\). Within one slot the vertices are parallel \(n\)-cells, so these assignments have exactly the required faces. They extend to model maps by the free universal property.

For each \((n+1)\)-dimensional generating edge \(e\) of \(K\), choose a cell \[ \alpha_e:e\longrightarrow gf(e) \qquad\text{of dimension }n+2\text{ in }A. \tag{5}\] Such a cell exists by the groupoid calculus of Section 2. Indeed, \(gf(e)\) represents a walk in the original tree with the same endpoints as \(e\). Here an inverse of a composite is expanded at the level of homotopy classes, using uniqueness of inverses in the hom-set groupoid. Successively delete backtracking pairs from this walk. A walk in a tree without backtracking is the unique simple path between its endpoints, here the edge \(e\). Associativity, units, and inverse cancellation hold for \((n+1)\)-cells modulo \((n+2)\)-cell homotopy, so the two cells represent the same class. The homotopy relation is given by existence of a single joining cell, giving Equation (5).

We next turn these homotopies on generators into a statement about the whole model. For every such edge \(e\), adjoin a duplicate \(e'\) with the same boundary and a cell \(\delta_e:e\to e'\) of dimension \(n+2\). Let \(Q\) be the resulting model and \(a_0:A\to Q\) its canonical map. These are finitely many \(J_{n+1}\) attachments, so \(a_0\in\mathcal W\) by the already proved higher-index case. Define a second model map \(a_1:A\to Q\) by fixing every generator through dimension \(n\) and sending \(e\) to \(e'\). This is permitted because \(A=F_q(K)\) and \(K\) has no generators above dimension \(n+1\). The face equations of this globular assignment are the only conditions needed to extend it to the full model.

There is a common retraction \(r:Q\to A\): keep the original generators, send \(e'\) to \(e\), and send \(\delta_e\) to a unit on \(e\). Thus \(ra_0=ra_1=\mathrm{id}_A\). Two-out-of-three gives first \(r\in\mathcal W\) and then \(a_1\in\mathcal W\). Likewise Equation (5) defines a model map \(h:Q\to A\) which is the identity on the original copy, sends \(e'\) to \(gf(e)\), and sends \(\delta_e\) to \(\alpha_e\). The free universal property gives \[ha_0=\mathrm{id}_A,\qquad ha_1=gf.\] It follows that \(h\in\mathcal W\) and \(gf\in\mathcal W\). This promotion uses only \(J_{n+1}\), not \(J_n\).

The map \(gf\) factors through the contractible model \(L\). Hence its map on components factors through a singleton and its maps on positive based homotopy groups factor through trivial groups. Since these maps are respectively bijective and isomorphisms, \(A\) has one component and trivial homotopy groups. It is nonempty, so it is contractible.

When \(q=n+1\), the attachments used above are precisely \(J_q\), whose case was proved in Lemma 13. They retain the duplicate \(q\)-generators, while the joining \((q+1)\)-cells are unique. The definitions of \(a_1,r,h\) still have exactly their stated universal properties. Thus this boundary case requires no additional induction step. ◻

Proof. Set \(S'=T_n(S)\). It contains exactly the same \(n\)-cells as \(S\), so the same duplicates and joins can be adjoined to either shape. In \(S'\) every slot at depth \(n\) is a linear string or a singleton. Adding one leaf and its edge at each vertex turns each such slot into a finite oriented tree. Thus \(H_\epsilon(S')\) is the free model on a tree diagram at depth \(n\), and is contractible by Proposition 15. The same argument allows independent orientations.

By Lemma 11, \(S'\to S\) is a finite composite of source attachments with indices strictly greater than \(n\). Those attachments add no further \(n\)-cells. Perform them after adjoining the fixed set of duplicates and joins. Their original attaching maps use the retained generators of \(S\) and their original faces, so the resulting model is exactly \(H_\epsilon(S)\) by the pushout universal properties. Therefore \(H_\epsilon(S')\to H_\epsilon(S)\) is upper \(J\)-cellular. Its source and all intermediate objects are cellular, so the descending induction hypotheses make it a weak equivalence. Contractibility follows from that of \(H_\epsilon(S')\). If the recursion ends before depth \(n\), there are no joins in that branch and it remains unchanged throughout. ◻

Proof. The ordinary skeleton \(\mathop{\mathrm{sk}}_\ell S\) is obtained from \(\mathop{\mathrm{sk}}_{\ell-1}S\) by attaching one globe along its boundary for each \(s\in S_\ell\). Both \(F\) and the construction \(P(-)\) in Equation (6) preserve these colimits. More explicitly, a map \(C_\ell(S)\to T\) consists of a map \(F(S)\to T\) and maps from its cylinder objects through level \(\ell\), compatible on faces and on endpoint \(\epsilon\). After specifying the same data through level \(\ell-1\), extending them at a particular cell \(s\) amounts to choosing a map \(P_\ell\to T\) with its values already prescribed on \(P(\partial d_\ell)\) and on the retained endpoint \(D_\ell\). Those prescribed values form precisely a map \(A_\ell^\epsilon\to T\). This is the universal property of Equation (13).

In particular, faces shared by two cells use the same map from the previous skeleton. No additional copy of a shared face is introduced. The argument concerns colimits of the specified cylinder objects, so it also applies when an earlier upper completion has attached cells of dimension less than its cylinder index.

Through dimension \(n-1\), all the cylinders are stationary. At dimension \(n\), each cell acquires one duplicate and one joining cell; the original higher cells retain their original boundaries. This proves \(C_n(S)=H_\epsilon(S)\), including the case \(\dim(S)<n\), in which there are no whiskers. The other two identities follow from \(\mathop{\mathrm{sk}}_{j-1}d_j=\partial d_j\) and \(\mathop{\mathrm{sk}}_{\dim(S)}S=S\), respectively. ◻

Proof. The objects \(P_j\) for \(j\le n\) are free globes and are contractible by Proposition 12. Proceed by induction on \(j>n\), handling both endpoints. By Lemma 17, \(A_j^\epsilon\) is obtained from \(H_\epsilon(d_j)\) by pushing out the maps \(A_\ell^\epsilon\to P_\ell\) on the boundary cells of dimensions \(n<\ell<j\), in increasing order of \(\ell\). At each dimension, attach its finitely many cells one at a time. The resulting iterated pushout is the coproduct pushout of Lemma 17, by its universal property. The starting object is cellular and contractible by Proposition 16. Each map used in this filtration is already an upper cellular weak equivalence by the induction on \(j\). Lemma 14 therefore makes every one of its pushouts a weak equivalence. All intermediate objects are cellular, so the lemma applies at every stage. It follows that \(A_j^\epsilon\) is contractible. When \(j=n+1\), this filtration has no intervening stages: \(A_{n+1}^\epsilon=H_\epsilon(d_{n+1})\).

The upper cellular map \(A_j^\epsilon\to P_j\) preserves all cells through dimension \(n\), by Lemma 10. Thus \(P_j\) is nonempty and inherits fillers of dimensions \(1,\ldots,n\) from \(A_j^\epsilon\). Its map to the terminal object lifts the upper boundary inclusions by construction, so it has every remaining boundary filler. Hence \(P_j\) is contractible. At \(n=0\), the inherited condition is simply nonemptiness. Both terminal maps are now weak equivalences, so \(A_j^\epsilon\to P_j\) is a weak equivalence. Its upper cellularity was established in Equation (11). This completes the induction on \(j\).

For a pasting scheme \(S\) with \(\dim(S)\ge n\), start with \(C_n(S)=H_\epsilon(S)\) and use the same filtration through all dimensions \(n<\ell\le\dim(S)\). It ends at \(P(S)\). Every step is again a cellular weak equivalence by Lemma 14; its cellular, contractible starting object therefore gives the assertion. If \(\dim(S)<n\), then \(P(S)=F(S)\), so Proposition 12 applies directly. ◻

Construction of the algebraic interpretation. Interpret the generators in the original free construction order of \(\mathcal C\). At each stage, the globular set \(\mathcal P Y\) already interprets the entire preceding theory, naturally in the full model \(Y\), and both endpoints preserve that preceding theory. This holds initially for the globular structure.

Consider a new generating filler \(\theta\), of output dimension \(j>0\), on a pasting-scheme arity \(S\). If \(j>q\), evaluate its already interpreted boundary and take its unique filler in \(\mathcal P Y\). The endpoint equations follow from the boundary equations and unique fillers in \(Y\). This is natural in \(Y\).

Suppose \(j\le q\). The generator condition gives \(\dim(S)\le j\), so Equation (16) applies. If \(j<n\), the entire tuple lies in stationary dimensions: \(P(S)=F(S)\) and \(P_j=D_j\). Use the original operation of \(Y\). Its prescribed boundary follows from the preceding endpoint compatibility, since the endpoint maps are identical isomorphisms on all the cell sets involved.

It remains to handle \(n\le j\le q\). View the given operation, in the fixed category of full models, as a map \[\theta:D_j\longrightarrow F(S).\] This map exists independently of the interpretation being constructed on \(\mathcal P Y\). Its required endpoint values are the two existing maps \[ e_\epsilon(S)\theta:D_j\longrightarrow P(S). \tag{17}\] The two face operations of \(\theta\) belong to the preceding theory. Evaluating either one on an \(S\)-tuple gives, naturally in \(Y\), a function \[\mathop{\mathrm{Hom}}_{\mathcal A_q}(P(S),Y) \longrightarrow\mathop{\mathrm{Hom}}_{\mathcal A_q}(P_{j-1},Y).\] By Yoneda, these functions are represented by maps \(P_{j-1}\to P(S)\). Their parallelism is an equation in the preceding theory, so they agree on all their common faces and give \[b_\theta:P(\partial d_j)\longrightarrow P(S).\] The previous endpoint compatibility says exactly that \[ b_\theta e_\epsilon(\partial d_j) =e_\epsilon(S)(\theta|_{\partial D_j}). \tag{18}\] Consequently \(b_\theta\) and the two maps in Equation (17) glue to a map \[ A_j^{01}\longrightarrow P(S). \tag{19}\]

The map \(A_j^{01}\to P_j\) is cellular for \(n\le j\le q\), and \(P(S)\) is contractible by Proposition 18. Its terminal map therefore lifts every boundary inclusion, and hence every cellular map. It extends Equation (19) to a map \(P_j\to P(S)\). Precomposition with this chosen map is the required operation on \(\mathcal P Y\). Its boundary and endpoint equations hold by construction.

In this step a face operation can be a composite of output dimension \(j-1\) whose arity \(S\) has height \(j\). Its evaluation and Yoneda representation use the whole preceding theory. Preservation of its generators makes the endpoints preserve all their composites and substitutions as well. The inequality \(\dim(S)\le j\) was used for the new generator; no smaller arity bound on its composite faces is needed.

Make the representing choices once, independently of \(Y\). Postcomposition by a map \(Y\to Z\) then preserves every chosen operation. At limit stages of the free theory, the compatible interpretations give the interpretation of its union. Freeness now provides a model of the full \(\mathcal C\), natural in \(Y\), and both endpoints are full model morphisms. The construction leaves the chosen globular set unchanged; it is therefore still \(q\)-coskeletal. ◻

Lifting for an individual endpoint. For \(j\le q\), an \(I_j\)-lifting problem against \(p_\epsilon\) specifies a boundary cylinder and one endpoint disk with matching endpoint boundary. By Equation (7), it is a map \(A_j^\epsilon\to Y\), and a solution is an extension to \(P_j\to Y\).

For \(j<n\), the map \(A_j^\epsilon\to P_j\) is the identity. For \(j=n\), it is one face inclusion \(D_n\to D_{n+1}\), which has a retraction given by a unit operation. For \(j>n\), it is an upper cellular weak equivalence by Proposition 18, and has a retraction by Lemma 14. Precomposing with these retractions gives the desired extensions into every \(Y\). For \(j>q\), the map \(I_j\) is an isomorphism in \(\mathcal A_q\). Thus both endpoints lift all \(I_j\), and belong to \(\mathcal W\) by Lemma 8. ◻

Lifting for the joint endpoint. A lifting problem against \(J_n\) consists of a map \(h:P_n\to Y\) and two maps \(a_0,a_1:D_{n+1}\to Y\) whose source faces are the two endpoints of \(h\). Its representing object is \[ B=P_n\amalg_{D_n\amalg D_n}(D_{n+1}\amalg D_{n+1}), \tag{20}\] where the attaching maps use the two endpoints of \(P_n\) and the source of each new disk. Since \(P_n=D_{n+1}\), its presentation in the depth-\(n\) slot has four \(n\)-cells and three \((n+1)\)-cells: \[h:x_0\longrightarrow x_1,\qquad a_0:x_0\longrightarrow y_0,\qquad a_1:x_1\longrightarrow y_1.\] For \(n>0\), the four \(n\)-cells have their common lower globular boundary. For \(n=0\), they are four ordinary vertices. The underlying graph is the tree \(y_0-x_0-x_1-y_1\). Thus \(B\) is cellular and contractible by Proposition 15.

The cylinder on the source \(n\)-face is already \(P_n\). Attach the missing comparison \(y_0\to y_1\), one \((n+1)\)-cell, to supply the cylinder on the target face. Together with the two endpoint disks this is exactly \(A_{n+1}^{01}\). Hence the natural map to \(P_{n+1}\) factors as \[B\longrightarrow A_{n+1}^{01} \longrightarrow P_{n+1},\] where the first map is one \(I_{n+1}\)-attachment and the second is the chosen upper completion. It is an upper cellular map between cellular contractible objects, so it is a weak equivalence and splits by Lemma 14. A retraction \(P_{n+1}\to B\), followed by the prescribed map \(B\to Y\), solves the lifting problem. This also applies when \(q=n+1\): the missing comparison is a legitimate \(I_q\)-attachment, and all subsequent required fillers are provided by the same construction. This completes the proof of Proposition 19. ◻

Completion of the descending induction. Let \(X\) be cellular in \(\mathcal A_q\), let \(a:D_n\to X\) be arbitrary, and form the algebraic pushout \[Y=X\amalg_{D_n}D_{n+1},\qquad i:X\longrightarrow Y.\] The unit on \(a\) gives the elementary retraction \(r:Y\to X\), with \(ri=\mathrm{id}_X\). Because \(p_0:\mathcal P X\to X\) lifts every boundary inclusion and \(X\) is cellular, there is a map \(h:X\to\mathcal P X\) with \(p_0h=\mathrm{id}_X\). Set \[u=p_1h:X\longrightarrow X, \qquad \bar u=ur:Y\longrightarrow X.\] Both endpoints are weak equivalences; thus two-out-of-three first gives \(h\in\mathcal W\) and then \(u\in\mathcal W\). Also \(\bar u i=u\).

Consider the square \[ \begin{tikzpicture}[baseline=(current bounding box.center), node distance=1.45cm and 3.2cm,>=Stealth] \node (a) {\(X\)}; \node (b) [right=of a] {\(\mathcal P Y\)}; \node (c) [below=of a] {\(Y\)}; \node (d) at (b |- c) {\(Y\times Y\).}; \draw[->] (a) -- node[above] {\(\mathcal P(i)h\)} (b); \draw[->] (a) -- node[left] {\(i\)} (c); \draw[->] (b) -- node[right] {\((p_0,p_1)\)} (d); \draw[->] (c) -- node[below] {\((\mathrm{id}_Y,i\bar u)\)} (d); \end{tikzpicture} \tag{21}\] Naturality and \(\bar u i=u\) give its commutativity explicitly: \[(p_0,p_1)\mathcal P(i)h=(i,iu) =(\mathrm{id}_Y,i\bar u)i.\] The right-hand map lifts \(J_n\) by Proposition 19, so it lifts its pushout \(i\). Indeed, restrict the top map along the given \(a:D_n\to X\), and restrict the bottom map along the new disk \(D_{n+1}\to Y\). Solve this \(J_n\)-square; its solution agrees with the original top map on \(D_n\), and the actual pushout universal property glues the two maps. This produces \(f:Y\to\mathcal P Y\) with \[p_0f=\mathrm{id}_Y,\qquad p_1f=i\bar u.\] This use of the pushout requires no condition on the selected cell \(a\) beyond being a model morphism from \(D_n\). Two-out-of-three again gives \[v:=i\bar u\in\mathcal W.\]

Finally, \(iu:X\to Y\) is a retract of \(v=iur:Y\to Y\) in the arrow category. The maps of arrows in the two directions have domain maps \(i\) and \(r\), respectively, and codomain map \(\mathrm{id}_Y\) in both cases. The identities \[vi=iu,\qquad (iu)r=v,\qquad ri=\mathrm{id}_X\] verify the two commuting squares and their identity composite. Retract closure gives \(iu\in\mathcal W\), and two-out-of-three with \(u\in\mathcal W\) gives \(i\in\mathcal W\). Every map in this argument is a morphism of the full algebraic models; the conclusion therefore includes all freely generated composites and coherence cells of the pushout, for the arbitrary attaching cell \(a\).

This proves the induction step at \(n\). Together with the top case established in the preceding section, descending induction proves the elementary expansion assertion for every index at this fixed cutoff \(q\). ◻

Proof of Theorem 1. Return to the original category \(\mathcal A\), and write \(i:X\to Y\) for the pushout in the theorem. Fix an instance of the exact-boundary test in dimension \(k\). Choose \(q\ge\max\{n+1,k+1\}\). By Lemma 9, the reflector \(R_q\) preserves the cellular presentation of \(X\) and the actual pushout defining \(Y\). The fixed-cutoff theorem therefore applies to \(R_q(i)\).

The reflector preserves all cells through dimension \(q\), with their face maps. Consequently the given boundary and target disk are unchanged by reflection. The source disk and its \((k+1)\)-cell homotopy supplied by the fixed-cutoff theorem are also in unchanged dimensions. They are therefore a source disk with the original exact boundary and an actual homotopy in \(Y\) before reflection. Proposition 5 proves that \(i\) is a weak equivalence. This holds for every \(k\), every \(n\ge0\), every cellular \(X\), and the arbitrary fixed coherator \(\mathcal C\), as required. ◻

Proof. Each \(J_j\) is a composite of two boundary attachments: an \(I_j\)-attachment adds the parallel \(j\)-cell, and an \(I_{j+1}\)-attachment adds the cell joining the two. Consequently \(J\subset I\text{-}\mathrm{cof}\). The lifting calculation of Lemma 8 gives \[ I\text{-}\mathrm{inj} =\mathcal W\cap J\text{-}\mathrm{inj}. \tag{22}\] Indeed an \(I\)-injective map satisfies the exact-boundary test and lifts \(J\); conversely, for a weak equivalence lifting \(J\), first lift a disk up to one higher homotopy and then lift that homotopy to correct the disk exactly.

The small object argument for \(I\) supplies a weak factorization system \[\bigl(I\text{-}\mathrm{cof},\ I\text{-}\mathrm{inj}\bigr)\] on all maps. In particular, factoring \(\varnothing\to X\) shows that every cofibrant \(X\) is a retract of a cellular object: the cofibrancy of \(X\) provides a section of the resulting trivial fibration onto \(X\). The converse follows from closure of the left lifting class under retracts.

Theorem 1 extends from cellular starts to cofibrant starts. To see this explicitly, choose a retract diagram \(X\xrightarrow{u}Z\xrightarrow{v}X\), with \(vu=\mathrm{id}_X\) and \(Z\) cellular. Given \(a:D_j\to X\), form the two expansions \[X^+=X\amalg_{D_j,a}D_{j+1}, \qquad Z^+=Z\amalg_{D_j,ua}D_{j+1}.\] The maps \(u,v\), together with the identity on the new \(D_{j+1}\), induce maps \(X^+\to Z^+\to X^+\) whose composite is the identity. Thus \(X\to X^+\) is a retract of \(Z\to Z^+\) in the arrow category and belongs to \(\mathcal W\).

Every relative \(J\)-cell map with cofibrant domain is therefore a weak equivalence. Cofibrancy is preserved at each stage because every \(J_j\) is an \(I\)-cofibration. At successor stages use the preceding paragraph, and at limit stages use the filtered-colimit closure of \(\mathcal W\) from Lemma 6. A set of simultaneous attachments can equally be attached in any well-order, so this also covers the coproducts used by the small object argument. The small object argument for \(J\) consequently factors every map with cofibrant domain as \[X\xrightarrow{j}Z\xrightarrow{p}Y, \qquad j\in I\text{-}\mathrm{cof}\cap\mathcal W, \quad p\in J\text{-}\mathrm{inj}.\] As a relative \(J\)-cell map, \(j\) has the left lifting property against every fibration.

Conversely, let \(i:X\to Y\) be an \(I\)-cofibration and a weak equivalence, with \(X\) cofibrant. Apply this factorization to \(i\), writing \(i=pj\). Two-out-of-three puts \(p\) in \(\mathcal W\), so Equation (22) makes \(p\) \(I\)-injective. A lift of \(i\) against \(p\) exhibits \(i\) as a retract of \(j\). Hence every trivial cofibration with cofibrant domain lifts against every fibration.

These are precisely the required factorizations and lifting axioms: cofibration–trivial-fibration factorization and lifting hold without restriction, while trivial-cofibration–fibration factorization and lifting are required for cofibrant domains. Completeness and cocompleteness follow from the algebraic description of \(\mathcal A\); the retract and two-out-of-three axioms were proved in Lemma 6. Finally, the unit of a \(j\)-cell extends it along \(J_j\). Thus every map \(X\to 1\) is \(J\)-injective, and every object is fibrant. ◻

Proof. Let \(\mathcal A_{\mathrm{fin}}\) be a small skeleton of the full subcategory of finitely cellular \(\mathcal C\)-groupoids, with finite boundary-cell extensions as cofibrations and the restriction of \(\mathcal W\) as weak equivalences. Henry’s comparison uses the following three facts.

First, under the expansion assertion, \(\mathcal A_{\mathrm{fin}}\) is a cylinder category (Henry 2016, Proposition 5.3.6). The finite nature of its cylinders is explicit: a relative cylinder for the generating cofibration \(\partial D_j\to D_j\) is \[D_j\amalg_{\partial D_j}D_j \longrightarrow D_{j+1}\longrightarrow D_j.\] The first map is \(I_{j+1}\), and the source endpoint is \(J_j\); the last map is induced by a unit. The source endpoint is a weak equivalence by Theorem 1, and hence so is the last map. Finite relative cylinders are obtained by the finite cell induction of that proposition. Trivial cofibrations in this category have retractions by Corollary 20, since their domains are cofibrant and all objects are fibrant.

Second, the free construction of the original coherator identifies the completion of \(\mathcal A_{\mathrm{fin}}\) with \(\mathop{\mathrm{Mod}}(\mathcal C)\), equipped with precisely the structure in Corollary 20 (Henry 2016, Proposition 5.3.7). In this construction one begins with finite globular sets and adjoins the operations in the given free order of \(\mathcal C\). Thus the identification retains the chosen theory and its actual algebraic models. The generating cofibrations in the completion are the \(I_j\), and its generating trivial cofibrations are the relative-cylinder endpoints \(J_j\).

Third, the marked object \(D_0\) makes \(\mathcal A_{\mathrm{fin}}\) a cylinder coherator (Henry 2016, Corollary 5.3.12). In Henry’s terminology this means that the map from the free pre-cylinder category \(F_*\) on one object, selecting \(D_0\), is a trivial cofibration and that the target is a cylinder category (Henry 2016, Definition 5.1.1). The hypotheses used in this implication are the free cellular construction of \(\mathcal C\), the expansion assertion, and the homotopical terminality of \(D_0\). The first is part of Definition 2, the second is Theorem 1, and the third follows here also from Proposition 12: the map \(D_0\to1\) is \(I\)-injective by the boundary-filling characterization of contractibility. Every map \(A\to D_0\) therefore extends across every finite cellular cofibration \(A\to B\); this gives homotopical terminality inside \(\mathcal A_{\mathrm{fin}}\). More explicitly, the projection \(p:\mathcal A_{\mathrm{fin}}^{D_0}\to\mathcal A_{\mathrm{fin}}\) in Henry’s construction is an acyclic fibration by (Henry 2016, Proposition 4.4.4).² The relative cofibrancy of \(F_*\to\mathcal A_{\mathrm{fin}}\) from (Henry 2016, Proposition 5.3.7) therefore gives a section of \(p\) sending the marked \(D_0\) to its cylinder \((D_0,D_1)\). The lifting argument of (Henry 2016, Lemma 5.3.9) then gives the asserted cylinder-coherator property, as in (Henry 2016, Lemma 5.3.11 and Corollary 5.3.12).

Henry’s Theorem 5.1.2(5) now gives a fundamental-infinity-groupoid right Quillen equivalence from spaces to this completion, with geometric realization as its left adjoint. By the second step the completion is the original \(\mathop{\mathrm{Mod}}(\mathcal C)\) with its canonical weak equivalences. This proves the displayed statements and is the implication summarized in (Henry 2016, Corollary 5.3.13). ◻