Theory and Applications of Categories, Vol. 11, No. 8, 2003, pp. 185–211.

CUBICAL SETS AND THEIR SITE

MARCO GRANDIS AND LUCA MAURI

ABSTRACT. Extended cubical sets (with connections and interchanges) are presheaves on a ground category, the extended cubical site 𝕂, corresponding to the (augmented) simplicial site, the category of finite ordinals. We prove here that 𝕂 has characterisations similar to the classical ones for the simplicial analogue, by generators and relations, or by the existence of a universal symmetric cubical monoid; in fact, 𝕂 is the classifying category of a monoidal algebraic theory of such monoids. Analogous results are given for the restricted cubical site 𝕀 of ordinary cubical sets (just faces and degeneracies) and for the intermediate site 𝕁 (including connections). We also consider briefly the reversible analogue, !𝕂.

1. Introduction

The category ˜△ of finite ordinals (and monotone mappings) is the basis of the presheaf category Smp^{∼} of augmented simplicial sets, i.e. functors X: ˜△^{op} → Set. It has well known characterisations, as:

(a) the subcategory of Set generated by finite ordinals, their faces and degeneracies,

(b) the category generated by such faces and degeneracies, under the cosimplicial relations,

(c) the free strict monoidal category with an assigned internal monoid.

The second characterisation is currently used in the description of an augmented simplicial set as a sequence of sets with faces and degeneracies, subject to the (dual) simplicial relations.

Cubical sets have also been considered; the main advantage, perhaps, can be traced back to the fact that cubes are closed under products, while products of tetrahedra have to be “covered” with tetrahedra; this advantage appears clearly when studying singular homology based on cubical chains, (cf. Massey [28]). Various works have proved the importance of adding, to the ordinary structure provided by faces and degeneracies, the connections (introduced in Brown-Higgins [4, 5, 6]; see also [33, 1, 12] and their references). Finally, the interest of adding interchanges and reversions can be seen in various works

Work supported by MIUR Research Projects Received by the editors 2002-03-08 and, in revised form, 2003-05-12. Transmitted by Ronald Brown. Published on 2003-05-15. 2000 Mathematics Subject Classification: 18G30, 55U10, 18D10, 18C10, 20F05, 20F10. Key words and phrases: Simplicial sets, cubical sets, monoidal categories, algebraic theories, gener-

ators and relations, word problem, classifying categories.

\begin{matrix}c \\ ◯ \end{matrix} Marco Grandis and Luca Mauri, 2003. Permission to copy for private use granted.

of the first named author on homotopy theory, based on a cylinder (or path) functor and its structure of cubical (co)monad (e.g., [14, 15, 16]). All these maps have their origin in the standard topological interval I = [0, 1] and its structure as an involutive lattice (cf. (12)).

Here, we give characterisations, similar to (a)–(c) above, for three “cubical sites”, 𝕀 ⊂ 𝕁 ⊂ 𝕂 ⊂ Set, whose objects are always the elementary cubes 2^{n} = {0, 1}^{n}. The first category is the ordinary (reduced) cubical site, generated by faces and degeneracies; 𝕁 includes connections, and 𝕂 also interchanges. The characterisation of the third, in Theorem 8.2, is perhaps the most important of the three; 𝕂 is:

(a) the subcategory of Set with objects 2^{n}, generated by faces, degeneracies, connections and interchanges;

(b) the subcategory of Set with objects 2^{n}, closed under the binary-product functor and generated by the basic faces (δ^{±}: 1 → 2), degeneracy (ε: 2 → 1), connections (γ^{±}: 2^{2} → 2) and interchange (σ: 2^{2} → 2^{2});

(c) the category generated by faces, degeneracies, connections and interchanges, under the extended cocubical relations (equations (5), (16), (28)–(30));

(d) the free strict monoidal category with an assigned symmetric cubical monoid (Section 6);

(e) the classifying category of the monoidal theory of symmetric cubical monoids (Section 10).

Again, this theorem gives a presentation of the extended cubical site 𝕂, and provides a definition of extended cubical sets (with connections and interchanges), by structural maps, under the dual relations. Note that 𝕂 is a symmetric monoidal category; however, in (d), we characterise it among arbitrary monoidal categories. The reason for this is that a cylinder endofunctor (with faces, degeneracies, connections and interchanges) in an arbitrary category C is a strict monoidal functor I^{∗} : 𝕂 → Cat(C, C), where Cat(C, C) is monoidal with respect to composition, though not symmetric in general.

References on cubical sets have been cited above; for simplicial sets see [30, 10, 13]. The characterisations of the category of finite ordinals can be found in Mac Lane’s text [27]; finite cardinals, the site of (augmented) symmetric simplicial sets, have been similarly characterised in [17]. For monoidal categories, see [27] and Kelly’s book [23]. Links with PRO’s, PROP’s, monoidal theories and rewrite systems will be given in the text.

Outline. The classical notion of an abstract interval in a monoidal category (with two faces and a degeneracy) is the starting point for considering ordinary, or restricted, cubical sets (with faces and degeneracies); we give an elementary characterisation of the corresponding restricted cubical site 𝕀, by cocubical relations or the existence of a universal bipointed object (Section 4). Then, we introduce cubical monoids in a monoidal category, proving the characterisations of the intermediate site 𝕁 (Section 5). Symmetric cubical monoids are dealt with in Section 6 and the main results recalled above on the extended cubical site 𝕂 are proved in Section 8. Then, we consider briefly the reversible analogue, !𝕂, which also has reversions (Section 9). In the appendix (Section 10) we show that the various notions of cubical monoids can be regarded as models of certain monoidal algebraic theories and that the cubical sites are the classifying categories for these theories. The reader can prefer to omit, at first, all references to such theories in the preceding sections, and go back to them when reading the Appendix.

It would be desirable to find a geometric characterisation of the maps in 𝕂. In fact, such maps preserve subcubes and the product order, but these conditions are not sufficient to characterise them (Section 8).

Notation. The term “graph” stands always for directed graph. In a monoidal category, the tensor powers A ⊗ … ⊗ A of an object are generally denoted as A^{n}. The binary weights α, β vary in the set {−, +}, or, when convenient, in 2 = {0, 1}; in both cases, −α denotes the “opposite” weight.

Acknowledgements. We are indebted to the editor, R. Brown, and to an exceptionally careful Referee, whose comments helped us to make many points clearer; the latter also provided relevant links with the theory of Rewrite Systems, in the proof of Theorem 5.1.

2. Geometric models

Combinatorial topology and combinatorial homotopy theory are based on three families of simple geometric models: the (standard) tetrahedra △^{n}, the cubes I^{n} = [0, 1]^{n} and the discs, or globes, D^{n}. Correspondingly, we have simplicial, cubical and globular sets, usually described as sequences of sets linked by mappings (faces and degeneracies, at least) satisfying suitable relations. Simplicial sets are presheaves X: △^{op} → Set on a very “natural” category, the simplicial site △ of positive finite ordinals [n] = {0, 1, …, n}, with monotone mappings; one might equivalently use for [n] the integral trace of the standard n-tetrahedron, △^{n} ∩ Z^{n+1} = {e_{0}, …, e_{n}}, i.e. the set of unit points of the cartesian axes.

In the cubical case, the objects of our site will be the elementary cubes 2^{n} = {0, 1}^{n} = I^{n} ∩ Z^{n}, i.e. the integral traces of the standard topological cubes; the maps will be conveniently defined, according to which kind of cubical sets we are considering: the ordinary ones (with faces and degeneracies), the intermediate ones (including connections), or the extended ones (also including interchanges). Finally, in the globular case, one can use the integral traces of the standard discs, D^{n} ∩ Z^{n} = {±e_{1}, …, ±e_{n}} (coinciding with the traces of the standard octahedra); but this will not be treated here (one can see [32]).

3. The pointwise embedding of a discrete site

Let C be a small category with a terminal object 1. A point (or global element, or global section) of a C-object C is a map x: 1 → C; the set of such maps yields the global section functor

Γ: C → Set,  Γ(C) = hom(1, C).  (1)

This functor is, trivially, injective on objects (since hom-sets in C are assumed to be disjoint). If it is also faithful, we shall call it the pointwise embedding of C (in Set); plainly, this condition is equivalent to saying that

(∗) for every C-object C, the family of its global elements x: 1 → C is jointly epi in C.

Another way of looking at this property is concerned with the presheaf category PSh(C) = Set^{C^{op}}. Then, the Yoneda embedding and the global section functor of PSh(C)

y: C → PSh(C),  y(C) = Ĉ = hom(−, C): C^{op} → Set,
Γ̂: PSh(C) → Set,  Γ̂(X) = X(1) = lim_{⟵}(X: C^{op} → Set),

(2)

give the global section functor Γ = Γ̂y of C, and it is easy to prove that Γ is faithful if and only if all the representable presheaves on C are simple (in the sense of [18], 1.3).

The simplicial sites have pointwise embedding, the ordinary one. We prove below that this is also true for the cubical sites 𝕀, 𝕁, 𝕂, which will thus be embedded in Set with objects 2^{n} (since, whatever be their definition, this is always the number of points of the object of “dimension n”). But it is false for the globular site, which can be easily embedded in Set with the objects considered in Section 2, but not as described above (all its objects of positive dimension have 2 vertices).

Finally, in order to characterise categories defined through generators and relations, we shall often use a general lemma, which can be sketched as follows. Note that, speaking of the special form of a composite of generators, we are not referring to the existence of some algorithm providing it: it is well known that a word problem, for monoids or categories, need not have a solution. In the sequel, we shall speak of canonical form when such an algorithm can be exhibited.

3.1. Lemma. [Special Form Lemma] Let G be a category generated by a subgraph G, whose maps satisfy in G a system of relations Φ. Then G is freely generated by G under such relations if and only if every G-map can be expressed in a unique special form f = g_{m} ⋯ g_{1}, as a composite of G-maps, and every G-factorisation f = g′_{n} ⋯ g′_{1} in G can be made special by applying the relations Φ finitely many times.

Proof. First, let us recall that a system of relations Φ on a graph G is a set of pairs of parallel morphisms in the free category Ĝ generated by G; a graph-morphism F: G → C with values in a category satisfies such relations if its extension to Ĝ identifies the morphisms of each pair. The category freely generated by G under Φ is produced by the universal such functor, mapping G to the quotient Ĝ/Φ (modulo the least congruence identifying all pairs of Φ).

Now, the necessity of the condition above is easily proved by choosing, arbitrarily, one special form in each equivalence class of Ĝ/Φ. Conversely, take a graph-morphism F: G → C, with values in an arbitrary category and satisfying the system of relations; this extends to at most one functor \overline{F}: G → C, letting it operate on special forms \overline{F} (g_{m} · . . . · g_{1}) = F (g_{m}) · . . . · F (g_{1}); this construction defines indeed a functor, since any composite gf in G is rewritten in special form using relations which “are preserved” in C.

4. The restricted cubical site 𝕀

Let 𝕀 be the subcategory of Set consisting of the elementary cubes 2^{n}, together with the maps f: 2^{m} → 2^{n} which delete some coordinates and insert some 0’s and 1’s (without modifying the order of the remaining coordinates).

𝕀 is a strict symmetric monoidal category; its tensor product 2^{p} □ 2^{q} = 2^{p+q} is induced by the cartesian product of Set, but is no longer a cartesian product in the subcategory (exponents denote tensor powers). (Note that 𝕀 is a PRO, i.e. a strict monoidal category whose monoid of objects is isomorphic to the additive monoid of natural numbers; cf. [26, 2].)

The object 2 is a bipointed object (both in (Set, ×) and (𝕀, □)), with (basic) faces δ^{α} and degeneracy ε

δ^{α}: 1 → 2,  ε: 2 → 1,  εδ^{α} = 1  (α = ±).  (3)

Higher faces and degeneracies are constructed from the structural maps, via the monoidal structure, for 1 ⩽ i ⩽ n and α = ±

\begin{aligned}δ_{i}^{α} & = 2^{i−1} □ δ^{α} □ 2^{n−i}: 2^{n−1} → 2^{n}, \\ ε_{i} & = 2^{i−1} □ ε □ 2^{n−i}: 2^{n} → 2^{n−1}, \end{aligned}  (4)

and the cocubical relations follow easily from the previous formulas:

\begin{aligned}δ_{j}^{β}δ_{i}^{α} & = & δ_{i+1}^{α}δ_{j}^{β}, & j ⩽ i \\ ε_{i}ε_{j} & = & ε_{j}ε_{i+1}, & j ⩽ i \\ & & δ_{i−1}^{α}ε_{j}, & j < i \\ ε_{j}δ_{i}^{α} & = & \{ & 1, & j = i \\ & & δ_{i}^{α}ε_{j−1}, & j > i. \end{aligned}  (5)

4.1. Lemma. [Canonical Form, for the restricted cubical site] Using (5) as rewriting rules (from left to right), each composite in Set of faces and degeneracies can be turned into a unique canonical factorisation (empty for an identity)

δ_{j_{1}}^{α_{1}} ⋯ δ_{j_{s}}^{α_{s}}ε_{i_{1}} ⋯ ε_{i_{r}}: 2^{m} → 2^{m−r} → 2^{n},  \begin{matrix}1 ⩽ i_{1} < ⋯ < i_{r} ⩽ m, \\ n ⩾ j_{1} > … > j_{s} ⩾ 1, \\ m − r = n − s ⩾ 0, \end{matrix}  (6)

consisting of a surjective composed degeneracy (a composition of ε’s, deleting the coordinates specified by indices), and an injective composed face (a composition of δ^{α}, inserting 0’s and 1’s in the specified positions).

Proof. Obvious.

4.2. Theorem. [The restricted cubical site] The category 𝕀 can be characterised as:

(a) the subcategory of Set with objects 2^{n}, generated by all faces and degeneracies (4);

(b) the subcategory of Set with objects 2^{n}, closed under the binary-product functor (realised as 2^{p} □ 2^{q} = 2^{p+q}), and generated by the basic faces (δ^{α}: 1 → 2) and degeneracy (ε: 2 → 1);

(c) the category generated by the graph (4), subject to the cocubical relations (5);

(d) the free strict monoidal category with an assigned internal bipointed object, (2; δ^{α}, ε);

(e) the classifying category of the monoidal theory I of bipointed objects.

The embedding 𝕀 → Set used above is the pointwise one (Section 3).

Proof. The characterisation (a) is already proved: every map of 𝕀 can clearly be factorised as in (6), in a unique way; therefore, (b) follows from the construction of higher faces and degeneracies as tensor products, in (4), while (c) follows from the Special Form Lemma 3.1. For (d), let A = (A, ⊗, E) be a strict monoidal category with an assigned bipointed object (A, δ^{α}, ε); then, defining higher faces and degeneracies of A as above, in (4)

\begin{aligned}δ_{i}^{α} & = δ_{n,i}^{α} = A^{i−1} ⊗ δ^{α} ⊗ A^{n−i}: A^{n−1} ⟶ A^{n}, \\ ε_{i} & = ε_{n,i} = A^{i−1} ⊗ ε ⊗ A^{n−i}: A^{n} ⟶ A^{n−1}, \end{aligned}  (7)

the cocubical relations are satisfied; therefore, we know that there is a unique functor F: 𝕀 → A sending 2^{n} to A^{n} and preserving higher faces and degeneracies. It is now sufficient to prove that this F is strictly monoidal (then, it will be the unique such functor sending 2 to A and preserving δ^{α}, ε); as we already know that F is a functor, our thesis follows from the following formulas

\begin{matrix}F (2^{p} □ 2^{q}) = F (2^{p+q}) = A^{p+q} = A^{p} ⊗ A^{q}, \\ F (ε_{n,i} □ 2^{p}) = F (ε_{n+p,i}) = ε_{n+p,i} = ε_{n,i} ⊗ A^{p}, \\ F (2^{p} □ ε_{n,i}) = F (ε_{n+p,i+p}) = ε_{n+p,i+p} = A^{p} ⊗ ε_{n,i}, \end{matrix}  (8)

(and the similar ones for faces), since the tensor product of arbitrary 𝕀-maps f = f_{p} ⋯ f_{1} and g = g_{q} ⋯ g_{1} (in canonical form) can be decomposed as

f □ g = (f_{p} □ 1) ⋯ (f_{1} □ 1)(1 □ g_{q}) ⋯ (1 □ g_{1}).  (9)

The meaning of statement (e) is explained in Section 10—see in particular the examples (a) in Section 10.1 and 10.2; its proof is given in Proposition 10.4. The last assertion follows immediately from Section 3.

4.3. Remark. (a) Our results, Lemma 4.1 and Theorem 4.2, not only give a reduced form for the maps of 𝕀, but solve the word problem for 𝕀, as presented above, by generators and relations (cf. [31, 3]). In fact we have proved that any (categorically well formed) word in faces and degeneracies can be rewritten in a unique canonical form, by applying finitely many times our relations (5), as “rewriting rules” (from left to right), so that all faces are taken to the left of all degeneracies, and both blocks are conveniently ordered. Similar results will be proved, much less trivially, for wider cubical sites — 𝕁 and 𝕂— in the next sections.

(b) A different global description of 𝕀, as embedded in Set^{op}, can be found in Crans’ thesis [8], Section 3.2. In fact, an 𝕀-map f: 2^{m} → 2^{n} can be represented by a mapping f^{∗}: \underline{n} → \underline{m} ∪ \{−, +\} (where \underline{n} = \{1, …, n\}) which reflects the order of \underline{m}, as in the following example

f: 2^{5} → 2^{7},  f = δ_{6}^{0}δ_{5}^{1}δ_{3}^{1}ε_{1} : (t_{1}, …, t_{5}) ↦ (t_{2}, t_{3}, 1, t_{4}, 1, 0, t_{5}),  (10)
f^{∗}: \underline{7} → \underline{5} ∪ \{−, +\},  1, 2, …, 7 ↦ 2, 3, +, 4, +, −, 5.  (11)

(f^{∗}: \underline{n} → \underline{m} ∪ \{−, +\} gives back f, sending t: \underline{m} → 2 to \underline{n} → \underline{m} ∪ \{−, +\} → 2, where the last map is t on \underline{m} and obvious on \{−, +\}.)

5. Connections and the intermediate cubical site

The set 2 = {0, 1} has a richer structure, as an involutive lattice, which can be described by the following structural mappings: faces, degeneracy, connections, interchange and reversion

\begin{matrix}\xymatrix{1 \ar[r]^{δ^{+}} \ar[r]_{δ^{−}} & 2 \ar[l]|{ε} & 2^{2} \ar[l]^{γ^{−}} \ar[l]_{γ^{+}}} & \xymatrix{2^{2} \ar[r]^{σ} & 2^{2}} & \xymatrix{2 \ar[r]^{ρ} & 2} \\ δ^{α}(0) = α, & σ(t, t′) = (t′, t), & ρ(t) = 1 − t, \\ γ^{−}(t, t′) = t ∨ t′, \\ γ^{+}(t, t′) = t ∧ t′. \end{matrix}  (12)

Deferring interchange and reversion to the next sections, let us note that we are not interested in the complete axioms of lattices (e.g., in the idempotence of the operations γ^{±}, or in their full absorption laws), but only in a part of them, corresponding to a cubical monoid in the sense of [14]: a set equipped with two structures of commutative monoid (∨, 0; ∧, 1), so that the unit of each operation is absorbent for the other (0 ∧ x = 0, 1 ∨ x = 1).

In a monoidal category A = (A, ⊗, E), an internal cubical monoid [14] is an object A with faces (or units) δ^{α}, degeneracy ε and connections (or main operations) γ^{α}

\xymatrix{E \ar[r]^{δ^{+}} \ar[r]_{δ^{−}} & A \ar[l]|{ε} & A ⊗ A \ar[l]^{γ^{−}} \ar[l]_{γ^{+}}}  (13)

satisfying the following axioms

εδ^{α} = 1, εγ^{α} = ε(ε ⊗ A) = ε(A ⊗ ε)  (degeneracy),
γ^{α}(γ^{α} ⊗ A) = γ^{α}(A ⊗ γ^{α})  (associativity),
γ^{α}(δ^{α} ⊗ A) = 1 = γ^{α}(A ⊗ δ^{α})  (unit),
γ^{β}(δ^{α} ⊗ A) = δ^{α}ε = γ^{β}(A ⊗ δ^{α}) (α ≠ β) (absorbing elements).

(14)

Higher connections are constructed from the basic ones, as in (4)

γ_{i}^{α} = A^{i−1} ⊗ γ^{α} ⊗ A^{n−i}: A^{n+1} → A^{n}  (1 ⩽ i ⩽ n; α = ±),  (15)

and the cocubical relations for connections follow from these constructions and the previous axioms:

\begin{matrix}γ_{j}^{β}γ_{i}^{α} = \begin{cases}γ_{i}^{α}γ_{j+1}^{β}, & j > i \\ γ_{i}^{α}γ_{i+1}^{α}, & j = i; α = β \end{cases} & ε_{j}γ_{i}^{α} = \begin{cases}γ_{i−1}^{α}ε_{j}, & j < i \\ ε_{i}ε_{i}, & j = i \\ γ_{i}^{α}ε_{j+1}, & j > i \end{cases} \\ γ_{j}^{β}δ_{i}^{α} = \begin{cases}δ_{i−1}^{α}γ_{j}^{β}, & j < i − 1 \\ 1, & j = i − 1, i; α = β \\ δ_{i}^{α}ε_{i}, & j = i − 1, i; α ≠ β \\ δ_{i}^{α}γ_{j−1}^{β}, & j > i. \end{cases} \end{matrix}  (16)

(The dual relations have appeared quite recently, in [1], Section 3; but a partial version with one connection can be found in [4], p. 235).

Let 𝕁 be the subcategory of Set consisting of the elementary cubes 2^{n}, together with the mappings generated by all faces, degeneracies and connections (γ_{i}^{α}: 2^{n+1} → 2^{n}). Note, again, that 𝕁 is a PRO.

We prove now that every 𝕁-map has a unique canonical factorisation, as in the following example

\begin{aligned}δ_{3}^{−}δ_{1}^{+}γ_{1}^{+}γ_{1}^{−}ε_{2}ε_{5} : (t_{1}, …, t_{5}) & ↦ (t_{1}, t_{3}, t_{4}) \\ & ↦ (t_{1} ∨ t_{3}) ∧ t_{4} \\ & ↦ (1, (t_{1} ∨ t_{3}) ∧ t_{4}, 0). \end{aligned}  (17)

5.1. Theorem. [Canonical form for the intermediate cubical site] Each 𝕁-map (composite of faces, degeneracies and connections) can be rewritten, using (5) and (16), as

\begin{matrix}f = (δ_{k_{1}}^{β_{1}} ⋯ δ_{k_{t}}^{β_{t}})(γ_{j_{1}}^{α_{1}} ⋯ γ_{j_{s}}^{α_{s}})(ε_{i_{1}} ⋯ ε_{i_{r}}): 2^{m} → 2^{p} → 2^{p−s} → 2^{n}, \\ 1 ⩽ i_{1} < ⋯ < i_{r} ⩽ m, 1 ⩽ j_{1} ⩽ … ⩽ j_{s} < p, n ⩾ k_{1} > ⋯ > k_{t} ⩾ 1, \\ (p = m − r, p − s = n − t ⩾ 0). \end{matrix} (18)

We obtain a unique, canonical form, adding the following condition on connections:

(∗) if j_{k} = j_{k+1} then α_{k} ≠ α_{k+1}.

This form consists of a (surjective) composed degeneracy ε = ε_{i_{1}} ⋯ ε_{i_{r}}, a (surjective) composed connection γ = γ_{j_{1}}^{α_{1}} ⋯ γ_{j_{s}}^{α_{s}} and an (injective) composed face δ = δ_{k_{1}}^{β_{1}} ⋯ δ_{k_{t}}^{β_{t}}.

Proof. First, we want to mention a relevant information due to the Referee. An alternative proof to the present one can be based on the theory of rewrite systems, originated in the framework of λ-calculus, cf. [11, 19]: one would reduce the argument to showing that all critical pairs (γ, γ′) are joinable, for suitable pairs of composed connections. This new proof would be clearer and placed in a well-established context. But we agree with the Referee’s suggestion of not modifying the line of our original proof, because the following case 𝕂 seems to be hardly solvable in the new line, and the techniques we shall use there “are best understood as extensions” of the ones we are using here.

Now, the proof. The existence the factorisation above is obvious, taking into account, for (∗), the fact that γ_{i}^{α}γ_{i}^{α} = γ_{i}^{α}γ_{i+1}^{α}. As to its uniqueness, the composed face δ: 2^{n−t} → 2^{n} (and its factorisation) is determined by the image of f, which has to be an (n−t)-face of 2^{n} (for some t ⩽ n); while the composed degeneracy ε: 2^{m} → 2^{m−r} (and its factorisation) is determined by the indices of the coordinates of (t_{1}, …, t_{m}) ∈ 2^{m} from which our mapping f does not depend (fδ_{i}^{α}ε_{i} = f). Since the former is injective and the latter surjective, also the composed connection γ is determined, and we are reduced to prove that, if the following factorisations

γ = γ_{i_{1}}^{α_{1}} ⋯ γ_{i_{s}}^{α_{s}} = γ_{j_{1}}^{β_{1}} ⋯ γ_{j_{s}}^{β_{s}}: 2^{p} → 2^{p−s}  \begin{matrix}(1 ⩽ i_{1} ⩽ … ⩽ i_{s} < p; \\ 1 ⩽ j_{1} ⩽ … ⩽ j_{s} < p), \end{matrix}  (19)

satisfy the condition (∗), then i = j and α = β, where i = (i_{1}, …, i_{s}) and so on. Since it is obviously true for s = 0, let us assume it holds up to s − 1 and prove it for s.

The initial block of i will be the maximal initial segment (i_{1}, …, i_{q}) without holes: i_{k+1} coincides with i_{k} or i_{k} + 1 (1 ⩽ k < q). Concretely, it corresponds to a block of coordinates linked by connections; formally, it is determined by the mapping γ by the following computations. To begin with

\begin{aligned}ε_{i}γ & = γ_{i_{1}−1}^{α_{1}} ⋯ γ_{i_{s}−1}^{α_{s}}ε_{i}: 2^{p} → 2^{p−s−1} & (i < i_{1}), \\ ε_{i}γ & = ε_{i}ε_{i}γ_{i_{2}}^{α_{2}} ⋯ γ_{i_{s}}^{α_{s}} \\ & = ε_{i}ε_{i+1} ⋯ ε_{i+q}γ_{i_{q+1}}^{α_{q+1}} ⋯ γ_{i_{s}}^{α_{s}} \\ & = γ_{i_{q+1}−q−1}^{α_{q+1}} ⋯ γ_{i_{s}−q−1}^{α_{s}}ε_{i} ⋯ ε_{i+q} & (i = i_{1}), \end{aligned}  (20)

showing that ε_{i}γ does not depend on precisely one coordinate for i < i_{1}, but on q + 1 ⩾ 2 coordinates for i = i_{1}; therefore the sequences i and j must have i_{1} = j_{1} and the same length q ⩽ s of their initial block; moreover

γ_{i_{q+1}−q−1}^{α_{q+1}} ⋯ γ_{i_{s}−q−1}^{α_{s}}ε_{i} ⋯ ε_{i+q} = γ_{j_{q+1}−q−1}^{β_{q+1}} ⋯ γ_{j_{s}−q−1}^{β_{s}}ε_{i} ⋯ ε_{i+q},  (21)

whence, cancelling ε_{i} ⋯ ε_{i+q} and applying the inductive assumption, we get that the indices and weights involved above coincide. Cancelling the corresponding composed connection in (19), we have a similar equality for the initial blocks (where the index i_{1} = j_{1} is already determined)

\begin{matrix}γ′ = γ_{i_{1}}^{α_{1}} ⋯ γ_{i_{q}}^{α_{q}} = γ_{j_{1}}^{β_{1}} ⋯ γ_{j_{q}}^{β_{q}}: 2^{p} → 2^{p−q}, \\ i_{1} = j_{1}, \\ i_{k+1} − i_{k} ⩽ 1, j_{k+1} − j_{k} ⩽ 1 (1 ⩽ k < q). \end{matrix}  (22)

(Note that we cannot apply the inductive assumption to these blocks, because we do not know whether q < s.)

Let h ⩾ 1 be the greatest number such that i_{1} = i_{2} = … = i_{h}(= i); by (∗), the segment (α_{1}, …, α_{h}) is a sequence of alternating weights, α_{1} ≠ α_{2} ≠ … The mapping γδ_{i}^{α} can be computed as follows

γδ_{i}^{α} = \begin{cases}γ_{i_{1}}^{α_{1}} ⋯ γ_{i_{h−1}}^{α_{h−1}}γ_{i_{h+1}−1}^{α_{h+1}} ⋯ γ_{i_{q}−1}^{α_{q}}, & α = α_{h} \\ γ_{i_{1}}^{α_{1}} ⋯ γ_{i_{h−2}}^{α_{h−2}}ε_{i}γ_{i_{h+1}−1}^{α_{h+1}} ⋯ γ_{i_{q}−1}^{α_{q}} = γ_{i_{1}}^{α_{1}} ⋯ γ_{i_{h−2}}^{α_{h−2}}ε_{i}ε_{i+1} ⋯ ε_{i+q−h}, & h > 1, α ≠ α_{h} \\ δ_{i}^{α}ε_{i}ε_{i+1} ⋯ ε_{i+q−1}, & h = 1, α ≠ α_{1}. \end{cases}

(23)

Thus, the weight α_{h} and the number h are determined by the fact that γδ_{i_{1}}^{α} depends on each of its coordinates if α = α_{h}, while otherwise it is independent of, precisely, q+1−h ⩾ 1 of them. Therefore, j has the same initial block of equal indices j_{1} = j_{2} = ⋯ = j_{h}(= i) and α_{h} = β_{h}; computing γδ_{i}^{α} on both expressions, for α = α_{h} = β_{h}, we have

γ_{i_{1}}^{α_{1}} ⋯ γ_{i_{h−1}}^{α_{h−1}}γ_{i_{h+1}−1}^{α_{h+1}} ⋯ γ_{i_{q}−1}^{α_{q}} = γ_{j_{1}}^{β_{1}} ⋯ γ_{j_{h−1}}^{β_{h−1}}γ_{j_{h+1}−1}^{β_{h+1}} ⋯ γ_{j_{q}−1}^{β_{q}},  (24)

and applying the inductive assumption to this equality, we conclude that i = j and α = β.

5.2. Theorem. [The intermediate cubical site] The category 𝕁 is a strict symmetric monoidal category, with respect to the tensor product 2^{p} □ 2^{q} = 2^{p+q}. It can be characterised as:

(a) the subcategory of Set with objects 2^{n}, generated by all faces, degeneracies and connections;

(b) the subcategory of Set with objects 2^{n}, closed under the binary-product functor (realised as 2^{p} □ 2^{q} = 2^{p+q}), and generated by the basic faces (δ^{α}: 1 → 2), degeneracy (ε: 2 → 1), connections (γ^{α}: 2^{2} → 2);

(c) the category generated by the graph formed of faces, degeneracies and connections, subject to the cocubical relations (5) and (16);

(d) the free strict monoidal category with an assigned internal cubical monoid, namely (2; δ^{α}, ε, γ^{α});

(e) the classifying category of the monoidal theory J of cubical monoids.

The embedding 𝕁 → Set used above is the pointwise one (Section 3).

Proof. Follows from the previous theorem, as in Theorem 4.2. The monoidal theory of cubical monoids is described in Section 10.1, example (b). In view of 10.2(b), statement (e) coincides with Proposition 10.5.

6. Symmetric cubical monoids

In a monoidal category A = (A, ⊗, E), an internal symmetric cubical monoid is a cubical monoid A as in (13) with a symmetry (or interchange) σ

σ: A ⊗ A → A ⊗ A,  (25)

under the following axioms, added to (14) (the second is a Yang-Baxter condition on σ, see [24] and references therein)

\begin{aligned}σσ & = 1, & (σ ⊗ A)(A ⊗ σ)(σ ⊗ A) & = (A ⊗ σ)(σ ⊗ A)(A ⊗ σ), \\ (ε ⊗ A)σ & = A ⊗ ε, & σ(δ^{α} ⊗ A) & = A ⊗ δ^{α}, \\ γ^{α}σ & = γ^{α}, & σ(γ^{α} ⊗ A) & = (A ⊗ γ^{α})(σ ⊗ A)(A ⊗ σ). \end{aligned}  (26)

Higher interchanges are constructed in the usual way

σ_{i} = A^{i−1} ⊗ σ ⊗ A^{n−i}: A^{n+1} → A^{n+1}  (1 ⩽ i ⩽ n).  (27)

By the previous axioms, they satisfy the Moore relations:

\begin{aligned}σ_{i}σ_{i} & = 1, \\ σ_{i}σ_{j}σ_{i} & = σ_{j}σ_{i}σ_{j} & (i = j − 1), \\ σ_{i}σ_{j} & = σ_{j}σ_{i} & (i < j − 1), \end{aligned}  (28)

together with the mixed cocubical relations for interchanges:

\begin{aligned}& j < i & j = i & j = i + 1 & j > i + 1 \\ ε_{j}σ_{i} = & σ_{i−1}ε_{j} & ε_{i+1} & ε_{i} & σ_{i}ε_{j} \\ σ_{i}δ_{j}^{α} = & δ_{j}^{α}σ_{i−1} & δ_{i+1}^{α} & δ_{i}^{α} & δ_{j}^{α}σ_{i} \\ σ_{i}γ_{j}^{α} = & γ_{j}^{α}σ_{i+1} & γ_{i+1}^{α}σ_{i}σ_{i+1} & γ_{i}^{α}σ_{i+1}σ_{i} & γ_{j}^{α}σ_{i} \end{aligned}  (29)

γ_{i}^{α}σ_{i} = γ_{i}^{α}.  (30)

The extended cocubical relations will consist thus of (5) (for faces and degeneracies),

(16) (including connections) and the relations (28)–(30) above (including interchanges). ¿From (28), it follows that the symmetric group S_{n} operates on the tensor power A^{n}. (Recall that S_{n}, the group of automorphisms of the set {1, ...n}, is generated by the main transpositions σ_{i} = (i, i + 1), for 1 ⩽ i < n, under the relations (28); see Coxeter-Moser [7], 6.2; or Johnson [22], Section 5, Thm. 3.)

7. Interchanges and the extended cubical site

Let 𝕂 be the subcategory of Set consisting of the elementary cubes 2^{n}, together with the maps generated by faces, degeneracies, connections and main transpositions, produced by the interchange σ: 2 → 2 (12):

σ_{i} = 2^{i−1} □ σ □ 2^{n−i}: 2^{n+1} → 2^{n+1}  (1 ⩽ i ⩽ n).  (31)

By our previous remarks, the symmetric group S_{n} operates on 2^{n}. (𝕂 is a PROP; this means a strict monoidal category M with a faithful strict monoidal functor ⊔S_{n} → M, bijective on objects; the category ⊔S_{n} is the disjoint union of the groups S_{n}, with the obvious monoidal structure; cf [26, 21].)

Observe that the object 2 itself with the obvious operations is a symmetric cubical monoid in 𝕂, which will be called the generic symmetric cubical monoid.

To determine a canonical form for 𝕂-maps, it will be relevant to note the following example. The composed connection

γ_{1}^{−}γ_{2}^{+}γ_{4}^{+}γ_{5}^{+}γ_{8}^{−}: (t_{1}, …, t_{9}) ↦ (t_{1} ∨ (t_{2} ∧ t_{3}), t_{4} ∧ t_{5} ∧ t_{6}, t_{7}, t_{8} ∨ t_{9}),  (32)

is plainly invariant under the subgroup of permutations of S_{9} (acting on its domain, 2^{9}) generated by the main transpositions σ_{2} = (2, 3), σ_{4} = (4, 5), σ_{5} = (5, 6), σ_{8} = (8, 9).

In general, let a composed connection γ be given

γ = γ_{j_{1}}^{α_{1}} ⋯ γ_{j_{s}}^{α_{s}}: 2^{p} → 2^{p−s},  1 ⩽ j_{1} < … < j_{s} < p,  (33)

determined by a strictly increasing sequence j = (j_{1}, …, j_{s}) with weights α = (α_{1}, …, α_{s}) (and determining them, by Theorem 5.1). We shall use a subgroup S_{p}(j, α) of S_{p}, which is obviously contained in the subgroup of permutations which leave γ fixed

S_{p}(j, α) ⊂ S(γ) = {λ ∈ S_{p} | γλ = γ} ⊂ S_{p},  (34)

(and, likely, coincides with the latter; but we do not need this).

Namely, the subgroup S_{p}(j, α) is generated by those permutations σ_{i} (1 ⩽ i < p) such that one of the following conditions holds

− i is a j-index while i + 1 is not,

− i, i + 1 are j-indices with the same weight, α_{i} = α_{i+1}.

(35)

Equivalently, S_{p}(j, α) consists of the permutations which preserve the intervals of D_{p}(j, α): the latter is the decomposition of the (integral) interval [1, p] in a disjoint union formed of: (a) all maximal subintervals of type [j′, j′′] where all points are j-indices with the same α-weight, except possibly j′′ which need not be a j-index; (b) the remaining singletons. Thus, in case (32), we have j = (1, 2, 4, 5, 8) in [1, 9], with the following weights α and decomposition D_{9}(j, α)

1  ^{2}  ^{3}  ^{4}  ^{5}  ^{6}  ^{7}  ^{8}  ^{9}_{−}  _{+}  _{+}  _{+}  _{−}  α ∘ ∘ ∘ ∘ ∘ ∘ ∘ ∘ ∘ D_{9}(j, α)  (36)

the corresponding S_{9}(j, α) is precisely the subgroup of S_{9} considered above.

8. Main results, in the extended case

8.1. Theorem. [Canonical form for the extended cubical site] Each 𝕂-map (composite of faces, degeneracies, connections and interchanges) has a canonical factorisation

f = (δ_{k_{1}}^{β_{1}} ⋯ δ_{k_{t}}^{β_{t}})(γ_{j_{1}}^{α_{1}} ⋯ γ_{j_{s}}^{α_{s}})λ(ε_{i_{1}} ⋯ ε_{i_{r}}): 2^{m} → 2^{p} → 2^{p} → 2^{p−s} → 2^{n}, ; \begin{matrix}i ⩽ i_{1} < … < i_{r} ⩽ m, & λ ∈ S_{p} & (p = m − r), \\ 1 ⩽ j_{1} < … < j_{s} < p, & n ⩾ k_{1} > … > k_{t} ⩾ 1 & (p − s = n − t ⩾ 0), \end{matrix} (37)

where everything is unique, except the permutation λ ∈ S_{p} which is determined up to an arbitrary permutation of the subgroup S_{p}(j, α) ⊂ S_{p} defined in the previous section. Also λ is uniquely determined, provided we require that λ^{−1} be strictly increasing on the intervals of the decomposition D_{p}(j, α). (Then, according to terminology, λ and λ^{−1} are respectively called a shuffle and a deal for the decomposition D_{p}(j, α), or vice versa). The factorisation is again an epi-mono factorisation with image given by the composed face.

Proof. First, let us prove the existence of this factorisation. Invoking the preceding factorisation (18) and the rewriting rules (29) for interchanges, we only need to prove that here one can make the sequence j = (j_{1}, …, j_{s}) strictly increasing (in (18) it was weakly so). In fact, using interchanges and letting (30) intervene, one can replace any unwanted occurrence γ_{i}^{α}γ_{i}^{β} as follows

γ_{i}^{α}γ_{i}^{β} = γ_{i}^{α}σ_{i}γ_{i}^{β} = γ_{i}^{α}γ_{i+1}^{β}σ_{i}σ_{i+1}.  (38)

The fact that λ can be modified by an arbitrary permutation of the subgroup S_{p}(j, α) follows from γ_{i}^{α}σ_{i} = γ_{i}^{α} and the following two equations

γ_{i}^{α}γ_{j}^{β} = \begin{cases}γ_{i}^{α}σ_{i}γ_{j}^{β} = γ_{i}^{α}γ_{j}^{β}σ_{i}, & j > i + 1, \\ γ_{i}^{α}σ_{i}γ_{i+1}^{α} = γ_{i}^{α}γ_{i}^{α}σ_{i+1}σ_{i} = γ_{i}^{α}γ_{i+1}^{α}σ_{i+1}σ_{i} = γ_{i}^{α}γ_{i+1}^{α}σ_{i}, & j = i + 1; α = β, \end{cases} (39)

together with the classification of generators of S_{p}(j, α) in (35): use the first equation above for a generator σ_{i} of the first type (when i is a j-index but i + 1 is not); use the second equation for the second case (when i, i + 1 are j-indices with the same weight).

Finally, we must prove the uniqueness of the factorisation (37). Since the composed face δ_{k_{1}}^{β_{1}} ⋯ δ_{k_{t}}^{β_{t}} and the composed degeneracy ε_{i_{1}} ⋯ ε_{i_{r}} are determined as in Theorem 5.1, we are reduced to considering an identity

\begin{matrix}γ = γ′λ: 2^{p} → 2^{p−s}, & λ ∈ S_{p}, \\ γ = γ_{i_{1}}^{α_{1}} ⋯ γ_{i_{s}}^{α_{s}} & (1 ⩽ i_{1} < … < i_{s} < p), \\ γ′ = γ_{j_{1}}^{β_{1}} ⋯ γ_{j_{s}}^{β_{s}} & (1 ⩽ j_{1} < … < j_{s} < p), \end{matrix}  (40)

and proving that i = j, α = β, λ ∈ S_{p}(i, α). The delicate point will be controlling the permutation λ, by properties invariant up to permutation of coordinates.

(a). A particular case. Assume that i = j = (1, 2, ...p − 1), so that

γ = γ′λ: 2^{p} → 2,  γ = γ_{1}^{α_{1}} ⋯ γ_{p−1}^{α_{p−1}},  γ′ = γ_{1}^{β_{1}} ⋯ γ_{p−1}^{β_{p−1}}.  (41)

Since all i-indices are consecutive, D_{p}(i, α) is simply the decomposition of [1, p[ consisting of the maximal subintervals on which α is constant, with p added to the last of them. Let [i′, i′′] be one of these α-subintervals (whence, i′ < p) and i ∈ [i′, i′′]; then γδ_{i}^{α} = γδ_{i′}^{α} = ⋯ = γδ_{i′′}^{α} can be analysed as follows, depending on α

γδ_{i}^{α} = \begin{cases}γ_{1}^{α_{1}} ⋯ γ_{i′−1}^{α_{i′−1}}γ_{i′}^{α_{i′+1}} ⋯ γ_{p−2}^{α_{p−1}}, & α = α_{i} \\ γ_{1}^{α_{1}} ⋯ γ_{i′−2}^{α_{i′−2}}ε_{i′} ⋯ ε_{p−1}, & α ≠ α_{i}. \end{cases}  (42)

Note that the mapping γδ_{i}^{α} depends on each of its p − 1 coordinates if α = α_{i}, while it depends on exactly i′ −1 < p−1 of them if α ≠ α_{i}. But γδ_{i}^{α} = γ′λδ_{i}^{α} = γ′δ_{j}^{α}λ′, (j = λ(i)), and γ′δ_{j}^{α} depends on all its coordinates if α = β_{j}, on j′ − 1 otherwise (j′ being the initial endpoint of the β-subinterval containing j). Therefore, α_{i} = β_{j} and i′ = j′.

Moreover, letting i vary in the α-subinterval [i′, i′′], we have seen that j = λ(i) belongs to the β-subinterval beginning at j′ = i′, obviously fixed. In other words, λ takes the whole α-subinterval [i′, i′′] into a β-subinterval which begins, precisely, at i′ and has at least as many points as the former. Since this holds for all α-subintervals and λ is bijective, it follows that the decompositions D_{p}(i, α) and D_{p}(i, β) coincide and λ ∈ S_{p}(i, α); further, α_{i} = β_{λ(i)} = β_{i} for all i < p, so α = β.

(b) General case. Let us come back to the relation γ = γ′λ, as specified in (40). We can suppose that i_{s} ⩽ j_{s}. Since the thesis holds trivially for s = 0, when γ = γ′ = id and λ = id, we assume it holds up to s − 1 and prove it for s ⩾ 1.

Let h be the greatest integer ⩾ 1 such that i_{1} < i_{2} < … < i_{h} are consecutive; then

ε_{i}γ = \begin{cases}γ_{i_{1}−1}^{α_{1}} ⋯ γ_{i_{s}−1}^{α_{s}}ε_{i}: 2^{p} → 2^{p−s−1}, & i < i_{1} \\ \begin{aligned}ε_{i}ε_{i+1}γ_{i_{2}}^{α_{2}} ⋯ γ_{i_{s}}^{α_{s}} & = ε_{i} ⋯ ε_{i+h}γ_{i_{h+1}}^{α_{h+1}} ⋯ γ_{i_{s}}^{α_{s}} \\ & = γ_{i_{h+1}−h−1}^{α_{h+1}} ⋯ γ_{i_{s}−h−1}^{α_{s}}ε_{i} ⋯ ε_{i+h}, \end{aligned} & i = i_{1}, \end{cases}  (43)

so that the mapping ε_{i}γ = ε_{i}γ′λ does not depend on 1 coordinate for i < i_{1}, but on h + 1 coordinates for i = i_{1}; therefore the sequences i and j must have the same maximal initial segment of consecutive indices, (i_{1}, …, i_{h}) = (i, …, i + h) = (j_{1}, …, j_{h}), and the equality ε_{i}γ = ε_{i}γ′λ gives, for i = i_{1}

γ_{i_{h+1}−h−1}^{α_{h+1}} ⋯ γ_{i_{s}−h−1}^{α_{s}}ε_{i} ⋯ ε_{i+h} = γ_{j_{h+1}−h−1}^{β_{h+1}} ⋯ γ_{j_{s}−h−1}^{β_{s}}ε_{i} ⋯ ε_{i+h}λ.  (44)

This mapping, as expressed in the left member of (44), is independent of the coordinates t_{i}, …, t_{i+h} (and no other); therefore, the permutation λ must preserve the subset {i, ...i + h} (as well as its complement), which means that λ = λ′λ′′, where λ′ ∈ S_{p} permutes the subset {i, …, i+h} and λ′′ ∈ S_{p} its complement in [1, p]. It follows that λ′ can be omitted in (44) (but not in (40), generally!), while λ′′ can be moved to the left

γ_{i_{h+1}−h−1}^{α_{h+1}} ⋯ γ_{i_{s}−h−1}^{α_{s}}ε_{i} ⋯ ε_{i+h} = γ_{j_{h+1}−h−1}^{β_{h+1}} ⋯ γ_{j_{s}−h−1}^{β_{s}}\overline{λ′′}ε_{i} ⋯ ε_{i+h}: 2^{p} → 2^{p−s−1}; (45)

more precisely, \overline{λ′′} ∈ S_{p−h−1} is the permutation λ′′ transferred to the set [1, p−h−1] by the surjective mapping which omits the indices {i, ...i + h}, ε_{i} ⋯ ε_{i+h}: [1, p] → [1, p − h − 1]. Cancelling the latter, a surjection, we have

γ_{i_{h+1}−h−1}^{α_{h+1}} ⋯ γ_{i_{s}−h−1}^{α_{s}} = γ_{j_{h+1}−h−1}^{β_{h+1}} ⋯ γ_{j_{s}−h−1}^{β_{s}}\overline{λ′′}: 2^{p−h−1} → 2^{p−h−1−(s+h)},  (46)
γ_{i_{h+1}}^{α_{h+1}} ⋯ γ_{i_{s}}^{α_{s}} = γ_{j_{h+1}}^{β_{h+1}} ⋯ γ_{j_{s}}^{β_{s}}λ′′: 2^{p} → 2^{p−(s+h)}.  (47)

(The last passage comes from applying 2^{h+1} □ − to the preceding one.)

By the inductive assumption, (i_{h+1}, …, i_{s}) = (j_{h+1}, …, j_{s}), the corresponding terminal segments of α and β coincide as well, and λ′′ ∈ S_{p}(i_{h+1} …, i_{s}; α_{h+1} …, α_{s}). Rewriting the equality γ = γ′λ as below, transferring λ′ to \overline{λ′} and cancelling the epimorphism of (47), we have that

(γ_{i_{1}}^{α_{1}} ⋯ γ_{i_{h}}^{α_{h}})(γ_{i_{h+1}}^{α_{h+1}} ⋯ γ_{i_{s}}^{α_{s}}) = (γ_{i_{1}}^{β_{1}} ⋯ γ_{i_{h}}^{β_{h}})\overline{λ′}(γ_{j_{h+1}}^{β_{h+1}} ⋯ γ_{j_{s}}^{β_{s}})λ′′,  (48)
γ_{i_{1}}^{α_{1}} ⋯ γ_{i_{h}}^{α_{h}} = γ_{i_{1}}^{β_{1}} ⋯ γ_{i_{h}}^{β_{h}} \overline{λ′}: 2^{p−s+h} → 2^{p−s},  (49)
γ_{i_{1}}^{α_{1}} ⋯ γ_{i_{h}}^{α_{h}} = γ_{i_{1}}^{β_{1}} ⋯ γ_{i_{h}}^{β_{h}}λ′: 2^{p} → 2^{p−h}.  (50)

(For the last passage, apply − □ 2^{s−h}.)

Now, we cannot invoke again the inductive assumption, since we do not know whether k < s. But, recalling that i_{1}, …, i_{h} are consecutive, we can easily reduce (50) to case (a) (i.e., i_{1} = 1), applying degeneracies. Therefore, also the initial segments of α and β coincide (this was already known for i and j) and λ′ ∈ S_{p}(i_{1}, …, i_{h}; α_{1}, …, α_{h}). Finally, λ = λ′λ′′ ∈ S_{p}(i_{1}, …, i_{s}; α_{1}, …, α_{s}).

8.2. Theorem. [The extended cubical site] The category 𝕂 can be characterised as:

(a) the subcategory of Set with objects 2^{n}, generated by all faces, degeneracies, connections and interchanges (31);

(b) the subcategory of Set with objects 2^{n}, closed under the binary-product functor (realised as 2^{p} □ 2^{q} = 2^{p+q}), and generated by the basic faces, degeneracy, connections and interchange (δ^{α}, ε, γ^{α}, σ; cf. (12));

(c) the category generated by the graph formed with faces, degeneracies, connections and interchanges, subject to the extended cocubical relations (5), (16), (28)–(30);

(d) the free strict monoidal category with an assigned internal symmetric cubical monoid, (2, δ^{α}, ε, γ^{α}, σ);

(e) the classifying category of the monoidal theory K of symmetric cubical monoids.

The embedding 𝕂 → Set used above is the pointwise one (Section 3).

Proof. 𝕂 is defined as described in (a), which is plainly equivalent to (b). The equivalence of (a), (c), (d) follows from the previous theorem, as in Theorem 4.2. Finally, the theory of symmetric cubical monoids is defined in 10.1(c); the equivalence between its models and symmetric cubical monoids, as defined in Section 6, is explained in 10.2(c); thus, statement (e) reduces to Proposition 10.6.

8.3. Remark. Define a subcube of 2^{n} to be any n-ary product of objects {0}, {1}, 2, i.e. the image of any composed face δ_{j_{1}}^{α_{1}} ⋯ δ_{j_{s}}^{α_{s}}: 2^{n−s} → 2^{n}. The image of a map of 𝕂 is a subcube (by Theorem 8.1), hence any mapping of 𝕂 takes subcubes to subcubes by direct image and preserves the product order. However, these properties are not sufficient to characterise our mappings in Set. For a counterexample, consider the function φ: 2^{3} → 2 defined by the formula

φ(x_{1}, x_{2}, x_{3}) = (x_{1} ∧ x_{2}) ∨ (x_{1} ∧ x_{3}) ∨ (x_{2} ∧ x_{3}),  (51)

and represented graphically by the diagram below; φ attains value 0 on hollow nodes and 1 on filled nodes.

[figure: •; •; ∘; •; ∘; •; ∘; ∘]  (52)

It is clear that φ preserves order and subcubes; however, it does not belong to 𝕂. If it did, we could apply the factorisation Theorem 8.1 to obtain a canonical factorisation of φ. However, in this factorisation no degeneracy can occur as φ depends on all variables. The symmetry can be taken to be the identity, as all the variables appear symmetrically. And no face can appear as φ is surjective. In other words, φ should be a composite connection. However, were this the case, φ should be of the form x_{i} ∧ (…) or x_{i} ∨ (…), with the outer terms possibly permuted. In the first case the set of points on which φ is true would be confined to a 2-face; in the second it would contain a 2-face. And the diagram above shows that this is not the case.

9. The reversion

We end by dealing briefly with the reversion ρ: 2 → 2 (12), and the reversible extended cubical site !𝕂 which it produces. In a monoidal category A = (A, ⊗, E), an involutive symmetric cubical monoid is a symmetric cubical monoid A with involution (or reversion)

ρ: A → A,  (53)

under the following additional axioms (after (14) and (26))

\begin{aligned}ρρ & = 1, & ερ & = ε, & ρδ^{−} & = δ^{+}, \\ ργ^{−} & = γ^{+}(ρ ⊗ ρ), & σ(A ⊗ ρ) & = (ρ ⊗ A)σ. \end{aligned}  (54)

Higher reversions are constructed as usual

ρ_{i} = A^{i−1} ⊗ ρ ⊗ A^{n−i}: A^{n} → A^{n}  (1 ⩽ i ⩽ n),  (55)

and satisfy the following additional relations (after (5), (16), (28)–(30))

\begin{matrix}ρ_{i}ρ_{j} = \begin{cases}1, & i = j \\ ρ_{j}ρ_{i}, & i ≠ j \end{cases}  ε_{j}ρ_{i} = \begin{cases}ε_{i}, & i = j \\ ρ_{i}ε_{j}, & i ≠ j \end{cases}  ρ_{i}δ_{j}^{α} = \begin{cases}δ_{j}^{α}ρ_{i−1}, & j < i \\ δ_{i}^{−α}, & j = i \\ δ_{j}^{α}ρ_{i}, & j > i \end{cases} \\ ρ_{i}γ_{j}^{α} = \begin{cases}γ_{j}^{α}ρ_{i+1}, & j < i \\ γ_{i}^{−α}ρ_{i}ρ_{i+1}, & j = i \\ γ_{j}^{α}ρ_{i}, & j > i \end{cases}  ρ_{i}σ_{j} = \begin{cases}σ_{j}ρ_{i}, & j < i − 1 or j > i \\ σ_{j}ρ_{j}, & j = i − 1 \\ σ_{i}ρ_{i+1}, & j = i. \end{cases} \end{matrix}  (56)

!𝕂 will thus be the subcategory of Set consisting of the elementary cubes 2^{n}, together with the maps generated by faces, degeneracies, connections, main transpositions and reversions

ρ_{i} = 2^{i−1} □ ρ □ 2^{n−i}: 2^{n} → 2^{n}  (1 ⩽ i ⩽ n).  (57)

Using the previous relations, all such maps can be rewritten in the following form, under the same restrictions of the canonical form in 𝕂; moreover, μ is a composed reversion

f = (δ_{k_{1}}^{β_{1}} ⋯ δ_{k_{t}}^{β_{t}})(γ_{j_{1}}^{α_{1}} ⋯ γ_{j_{s}}^{α_{s}})λμ(ε_{i_{1}} ⋯ ε_{i_{r}}): 2^{m} → 2^{p} → 2^{p} → 2^{p−s} → 2^{n}.  (58)

Proving a “canonical form theorem”, as in the previous cases, would produce also here a characterisation theorem for !𝕂. (Because of (56), one can see that 2^{n} is acted upon by the hyperoctahedral group (Z/2)^{n} ⋊ S_{n}, the group of isometries of the n-cube; one might say that !𝕂 is a “PROC”, where C stands for cube.)

As for the other cubical sites, there is a monoidal algebraic theory !K of involutive symmetric cubical monoids. This is obtained from K adding a unary operation ¬ and the axioms listed in (70), which correspond to the algebraic part of (54). Involutive symmetric cubical monoids in a monoidal category A are then precisely the models of !K in A. Since we do not have a canonical form theorem, however, the arguments used in Section 10 cannot be applied to prove that !𝕂 is the classifying category of !K. Nevertheless, a classifying category of !K can be constructed syntactically and will be proved to be equivalent to !𝕂 [29]. It follows that !𝕂, defined above as a subcategory of Set, is the category generated by faces, degeneracies, connections, interchanges and reversions under the relations (5), (16), (28)–(30), (56); so that the corresponding cubical sets are indeed functors on !𝕂^{op}.

Again, the mappings of !𝕂 preserve subcubes (though not the order), but this property does not characterise them. For a counterexample, consider the arrow f: 2^{2} → 2 depicted below, where f attains value 0 on hollow nodes and 1 on filled nodes.

\xymatrix{• \ar[r] & ∘ \\ ∘ \ar[r] \ar[u] & • \ar[u]}  (59)

If f were in !𝕂 it could be written, by (58), either as t_{1} ∧ t_{2} or as t_{1} ∨ t_{2} where each t_{i} is either a variable or its negation. In the first case, f would attain value 1 on a single point; in the second on 3 points. And this is false.

10. Appendix: monoidal algebraic theories

In this section we provide an analysis of the cubical sites from a logical point of view. We show how the various classes of cubical monoids can be interpreted as models of suitably defined monoidal algebraic theories and how the corresponding cubical sites can be interpreted as classifying categories for these theories. This allows to recover the universal property of the cubical sites and to exhibit them as presentation-free versions of the theories. The exposition is modelled on the case of algebraic theories in cartesian categories [9, 20, 25] with the necessary generalisations; some of the ideas behind the analysis can be found in [2] and [21]. For conciseness, we restrict here to the framework needed to discuss the cubical sites. Thus, the signatures are single sorted and the languages only allow weakening and exchange as structural rules; moreover, we focus essentially on the semantical aspects of the theory. For a more general analysis, the reader is referred to [29].

10.1. Monoidal languages. Let Σ be a finitary, single sorted, algebraic signature. From Σ and from a countable set of variables we define a monoidal language L. The raw terms of L are defined inductively via the BNF grammar

t := x | f(t, …, t).  (60)

Note that we treat individual constants as a special case of functional constants. The terms of L are sequents

(x_{1}, …, x_{n}) ⊢ t,  (61)

which are derivable in the term calculus described below. In the sequent (61), the context Γ = (x_{1}, …, x_{n}) is a finite sequence of distinct variables and t is a raw term. We will occasionally abbreviate the term (61) by t when the context is understood. Contexts can be concatenated, provided the variables remain distinct after concatenation; this condition will be tacitly assumed throughout. Note that we never mention types, as we are dealing with a single sorted signature.

There are two sets of rules for the term calculus: functional rules and structural rules. We always insist that the functional rules be present. However, only a subset of structural rules need to be present, so that the same signature Σ generates more than one monoidal language, depending on the subset we choose . The functional rules are

\frac{−}{x ⊢ x}  (variables),  (62)
\frac{Γ_{1} ⊢ t_{1}, …, Γ_{n} ⊢ t_{n}}{Γ_{1}, …, Γ_{n} ⊢ f(t_{1}, …, t_{n})}  (functional constants),  (63)

where f in (63) is a functional constant of arity n. The structural rules are

\frac{(…, x_{i−1}, x_{i+1}, …) ⊢ t}{(…, x_{i−1}, x_{i}, x_{i+1}, …) ⊢ t}  (weakening),  (64)
\frac{(…, x_{i}, x_{i+1}, …) ⊢ t}{(…, x_{i+1}, x_{i}, …) ⊢ t}  (exchange),  (65)
\frac{(…, x_{i}, x_{i+1}, …) ⊢ t}{(…, x_{i}, x̂_{i+1}, …) ⊢ t[x_{i}/x_{i+1}]}  (contraction).  (66)

The language L is purely monoidal when only the functional rules are allowed in the term calculus. By contrast, L is a monoidal language with weakening when both the functional rules and weakening (64) are allowed. The terminology for the other structural rules is similar. The contraction rule (66) is mentioned here only for completeness and will play no role. The formulas of L are sequents

Γ ⊢ t_{1} = t_{2},  (67)

for which both Γ ⊢ t_{1} and Γ ⊢ t_{2} are derivable in the term calculus. Again, the context in formulas will often be dropped. Note that the formulas of a purely monoidal language have substantial limitations, as the variables declared in Γ are required to occur both in t_{1} and t_{2} exactly once and exactly in the order in which they have been declared. Thus, formulas like x ∧ ⊥ = ⊥ and x ∧ y = y ∧ x are not expressible if L is purely monoidal. In fact, structural rules are introduced precisely to account for formulas of this type. Weakening allows dummy variables, which are declared in the context but which do not explicitly appear in the raw terms, as in the right member of (x) ⊢ x ∧ ⊥ = ⊥. Exchange allows variables to appear in an order different from the one declared in the context, as in (x, y) ⊢ x∧y = y ∧x. Finally, contraction is intended to allow repetitions of variables. A monoidal algebraic theory T is assigned by a set of formulas in L, the axioms. The theorems of T are generated from the axioms by means of equality, substitution and structural rules; the reader is referred to [29] for more details. Here are the theories of interest to us.

(a) The theory I of bipointed objects. Here Σ = {⊤, ⊥} is the signature consisting of two individual constants and L is the monoidal language with weakening generated by Σ. The terms of L are thus given by the two individual constants and by the variables, over a possibly weakened context. I is formulated in L and has no axiom.

(b) The theory J of cubical monoids. Here Σ = {⊤, ⊥, ∧, ∨}, where meet and join are binary functional constants and L is the monoidal language with weakening generated by Σ. The axioms of J are:

(x ∧ y) ∧ z = x ∧ (y ∧ z), (x ∨ y) ∨ z = x ∨ (y ∨ z) (associativity),
x ∧ ⊤ = x = ⊤ ∧ x,  x ∨ ⊥ = x = ⊥ ∨ x  (unit),
⊥ ∧ x = ⊥ = x ∧ ⊥,  ⊤ ∨ x = ⊤ = x ∨ ⊤  (absorbing element).

(68)

Note that the axioms have been stripped of their context; this is (x, y, z) for associativity and (x) in the other cases.

(c) The theory K of symmetric cubical monoids. Σ is the signature of cubical monoids; the language L, however, is the monoidal language with weakening and exchange generated by Σ. The axioms of K are those listed in (68) supplemented by

x ∧ y = y ∧ x,  x ∨ y = y ∨ x  (commutativity).  (69)

(d) The theory !K of involutive, symmetric, cubical monoids. Here Σ = {⊤, ⊥, ∧, ∨, ¬}, where negation is a unary functional constant. The language L is again the monoidal language with weakening and exchange generated by Σ. The axioms of !K are those in (68) and (69) supplemented by

¬¬x = x  (involution),
¬(x ∨ y) = ¬x ∧ ¬y, ¬(x ∧ y) = ¬x ∨ ¬y (De Morgan),
¬⊤ = ⊥.

(70)

The use of the weakening rule in the language of bipointed objects will be justified from a semantical point of view. Note also that in the theory of involutive symmetric cubical monoids, half of De Morgan’s axiom is redundant in presence of the involution axiom.

10.2. Monoidal semantics. Monoidal languages are intended to be interpreted in monoidal categories. When structural rules are present, the background category is required to have additional structure. However, this additional structure is “local” in character. This means that, for example, we want to be able to interpret symmetric monoids in monoidal categories without requiring the category to be symmetric, as was explained in the introduction. Rather, we wish to impose the symmetry conditions only on the data which interpret the monoid.

We fix a monoidal category V; its associativity and unit isomorphisms are always understood and do not appear explicitly in the formulas and diagrams below; this simplifies the notation and does not cause any problem in view of the coherence theorem for monoidal categories. Assume first that L is a purely monoidal language generated by a signature Σ. An L-structure in V is assigned by an object M ∈ V and by an arrow

[[f]]: M^{n} → M  (71)

for every function symbol f of arity n in Σ; we say briefly that M is an L-structure. Every L-term (x_{1}, …, x_{n}) ⊢ t can then interpreted by an arrow

[[t]] = [[(x_{1}, …, x_{n}) ⊢ t]]: M^{n} → M.  (72)

The interpretation is inductive on the derivation of the term: variables are interpreted as identities, and the rule for functional constants is interpreted using composition as in the following diagram.

\xymatrix{M^{m} \ar[dr]_{_{[[t_{1}]] ⊗··· ⊗ [[t_{n}]]}} \ar@{.>}[rr]^{[[f(t_{1},...,t_{n})]]} &  & M \\  & M^{n} \ar[ur]_{[[f]]}}  (73)

When L admits structural rules, the definition of an L-structure M requires the assignments in (71) supplemented by the data below.

∘ If L admits weakening, we require the existence of an arrow π: M → 1 to the unit of the tensor which is compatible with the interpretation of all functional constants. This means that for every function symbol f of arity n there is a commutative diagram

\xymatrix{M^{n} \ar[r]^{[[f]]} \ar[dr]_{π^{n}} & M \ar[d]^{π^{1}} \\  & 1}  (74)

The case of individual constants is included provided we let π^{0} = 1. We refer to π as the interpretation of weakening in M. The intended meaning of condition (74) is that applying f and discarding the result is equivalent to discarding the input data of f.

∘ If L admits exchange, we require the existence of an arrow σ: M^{2} → M^{2}, which is involutive, satisfies the Yang-Baxter equation in (26), and is natural with respect to the interpretation of functional constants, in the sense that the diagram

\xymatrix{M^{n} ⊗ M \ar[r]^{(1,2,...,n+1)} \ar[d]_{[[f]] ⊗ 1} & M ⊗ M^{n} \ar[d]^{1 ⊗ [[f]]} \\ M ⊗ M \ar[r]_{(1,2)} & M ⊗ M}  (75)

commutes for every functional constant f of arity n. Note that the horizontal arrows can be written as permutations because the involution and Yang-Baxter axioms imply that the symmetric group S_{n} operates on the tensor power M^{n}, as already observed in Section 6. We refer to σ as the interpretation of exchange in M.

∘ If L admits contraction, we require the existence of an arrow △: M → M ⊗ M satisfying appropriate conditions.

Finally, when more than one structural rule is used in the term calculus, we impose compatibility condition between the arrows interpreting the structural rules. In the case of weakening and exchange — the only one we will consider here — the compatibility condition is given by the commutative diagram

\xymatrix{M ⊗ M \ar[rr]^{σ} \ar[dr]_{1 ⊗ π} &  & M ⊗ M \ar[dl]^{π ⊗ 1} \\  & M}  (76)

We can now complete the rules for interpretation of terms when L admits structural rules. Weakening is interpreted by composition with π, exchange by composition with σ and contraction by composition with △, as shown in the diagrams below.

\xymatrix{M^{n} \ar@{.>}[rr]^{[[(...,x_{i},...)⊢t]]} \ar[dr]_{1 ⊗ π_{i} ⊗ 1} &  & M \\  & M^{n−1} \ar[ur]_{[[(...x̂_{i},...)⊢t]]}}  (weakening)  (77)

\xymatrix{M^{n} \ar[dr]_{(i,i+1)} \ar@{.>}[rr]^{[[(...,x_{i+1},x_{i},...)⊢t]]} &  & M \\  & M^{n} \ar[ur]_{[[(...,x_{i},x_{i+1},...)⊢t]]}}  (exchange)  (78)

\xymatrix{M^{n−1} \ar[dr]_{1 ⊗ △ ⊗ 1} \ar@{.>}[rr]^{[[(...,x_{i},x̂_{i+1},...)⊢t[x_{i}/x_{i+1}]]]} &  & M \\  & M^{n} \ar[ur]_{[[(...,x_{i},x_{i+1},...)⊢t]]}}  (contraction).  (79)

As usual, satisfaction of a formula in an L-structure M is defined setting

M ⊨ t_{1} = t_{2} ⇔ [[t_{1}]] = [[t_{2}]],  (80)

and M is a model of a theory T if all the axioms of T are satisfied by M. We discuss in some detail models of the theories defined in 10.1.

(a) Bipointed objects. Since the signature Σ of I has only two individual constants, the purely monoidal part of the model M is assigned by arrows [[⊤]], [[⊥]]: 1 ⇉ M. There is, however, an additional arrow π: M → 1 interpreting weakening. Compatibility of weakening with constants (74) amounts to the equations π∘[[⊤]] = 1 and π∘[[⊥]] = 1. Since I has no axiom, there is no further requirement and a model of I is precisely a bipointed object as defined in (3).

(b) Cubical monoids. The signature Σ of J has now two additional binary function symbols ∧ and ∨, so that M must provide additional arrows [[∧]], [[∨]]: M^{2} ⇉ M. Because of the two new operations, there are two additional compatibility equations for weakening, π ∘[[∧]] = π^{2} and π ∘[[∨]] = π^{2} from (74). These two equations are the degeneracy axioms in the original definition of a cubical monoid (14). The remaining axioms in (14) correspond to the axioms in (68), so that cubical monoids in V are precisely the models in V of J. As an example, we analyse in detail the first part of the absorbing element axiom: (x) ⊢ ⊥ ∧ x = ⊥. The interpretation [[(x) ⊢ ⊥ ∧ x]] of the first term is the composite arrow top and right in the diagram below, whereas [[(x) ⊢ ⊥]] requires weakening and is the composite left and below

\xymatrix{M \ar[r]^{[[⊥]] ⊗ 1} \ar[d]_{π} & M^{2} \ar[d]^{[[∧]]} \\ 1 \ar[r]_{[[⊥]]} & M}  (81)

Thus, [[(x) ⊢ ⊥ ∧ x]] = [[(x) ⊢ ⊥]] precisely when the diagram commutes and M ⊧ ⊥∧x = ⊥ precisely when the corresponding part of the axiom on absorbing elements in (14) is satisfied.

(c) Symmetric cubical monoids. The difference with cubical monoids is now the assumption that L admits exchange and that M also satisfies the commutativity axioms (69). The interpretation of exchange provides an arrow σ: M^{2} → M^{2} and the symmetry conditions are precisely the first two equations in (26). The compatibility condition of σ with the operations (75) corresponds to the fourth and sixth equation in (26), respectively for individual and binary functional constants. The third equation in (26) is the compatibility condition between weakening and exchange (76). Finally, the commutativity axiom (69) is the remaining fifth equation in (26). Thus, symmetric cubical monoids as defined in Section 6 are precisely the models of K.

The case of involutive, symmetric, cubical monoids is left to the reader as it does not present any new feature.

10.3. The classifying category. If M and N are L-structures in V, a morphism of L-structures is an arrow g: M → N in V commuting with the interpretation of all constants. That is, for every function symbol f of arity n, the diagram below commutes.

\xymatrix{M^{n} \ar[r]^{g^{n}} \ar[d]_{_{[[f]]_{M}}} & N^{n} \ar[d]^{_{[[f]]_{N}}} \\ M \ar[r]_{g} & N}  (82)

When L admits structural rules, g is also required to commute with the interpretation of the structural rules. L-structures in V and their morphisms form a category Str(L, V). If T is an algebraic theory in the language L, we write Mod(T, V) for the full subcategory of L-structures generated by the T-models. Every monoidal functor F: V → V′ preserves T-models and therefore induces a functor F_{∗}: Mod(T, V) → Mod(T, V′). Therefore, Mod(T, ) is a functor from monoidal categories to categories. When this functor is representable, we say that T admits a classifying category. Thus, T admits a classifying category when there exists a monoidal category T and a natural equivalence

E: hom(T, V) ⟶^{∼} Mod(T, V).  (83)

The identity on T then corresponds to a T-model G in T, called the generic T-model, and the functor E in (83) is evaluation at G. Every monoidal algebraic theory admits a classifying category [29]. However, our aim here is simply to show that the cubical sites are the classifying categories of the corresponding monoidal algebraic theories, and this can be proved directly using the results in the previous sections. We discuss the case of bipointed objects in detail. Observe first that the restricted site 𝕀 is a monoidal category and that 2 ∈ 𝕀 is a bipointed object with [[⊤]]_{2} = δ^{+}, [[⊥]]_{2} = δ^{−} and π_{2} = ε, as was remarked in Section 4.

10.4. Proposition. The restricted cubical site 𝕀 is a classifying category for the theory I of bipointed objects, and 2 is a generic model.

Proof. We prove that evaluation at 2 induces the equivalence E in (83). Since every monoidal category is tensor equivalent to a strict monoidal one ([24], corollary 1.4) we may assume that V is strict. Given M ∈ Mod(I, V), define a strict monoidal functor F: I → V setting F (2) = M, and mapping the interpretation of constants and of weakening in 2 to the corresponding arrows in M; this defines F uniquely in view of the factorisation Lemma 4.1 and clearly E(F) = M, so that E is surjective on objects.

To prove that E is full and faithful, let F, F′: 𝕀 → V be monoidal functors, M = F (2) and M′ = F′(2) the induced models and g: M → M′ a morphism of I-models. Let us first assume that the functors F and F′ are strict monoidal. If t: F → F′ is a monoidal transformation inducing g, then g = t_{2} and since all the objects of 𝕀 are of the form 2^{n} and t is monoidal, we must have t_{2^{n}} = t_{2}^{n} so that if t exists it is uniquely determined. It remains to prove that such t is natural; by the factorisation lemma, suffices to prove naturality with respect to the interpretation of constants and weakening. Naturality with respect to ⊤ amounts to prove the commutativity of the diagram

[figure: F (1); t_{1}; F [[⊤]]_{2}; F′(1); F′[[⊤]]_{2}; F (2); t_{2}; F′(2)]  (84)

By definition, the vertical arrows are [[⊤]]_{M} and [[⊤]]_{M′} and the bottom arrow is g; hence the square commutes because g is a morphism of models. The case of ⊥ and of weakening is similar. When the functors F and F′ are not strict it is necessary to insert associativity and unit isomorphisms: more precisely, t_{2^{n}} is canonically isomorphic to t_{2}^{n} and diagram (84) is isomorphic to the corresponding diagram between the models; in any case, this suffices to prove uniqueness of t and its naturality.

The same result holds for the sites 𝕁 and 𝕂; more precisely, 2 ∈ 𝕁 is a cubical monoid, 2 ∈ 𝕂 is a symmetric cubical monoid and the factorisation Theorems 5.1 and 8.1 give

10.5. Proposition. The site 𝕁 is a classifying category for the theory J of cubical monoids and 2 ∈ 𝕁 is a generic model.

10.6. Proposition. The site 𝕂 is a classifying category for the theory K of symmetric cubical monoids and 2 ∈ 𝕂 is a generic model.

The proofs do not present any new feature when compared with 10.4, and are therefore omitted. The situation is slightly different for involutive, symmetric, cubical monoids as the lack of a unique-factorisation theorem for !𝕂 does not allow us to use the same argument. Nevertheless, it will be proved in [29] that the classifying category of !K obtained by purely syntactical means is equivalent to !𝕂, which is therefore the classifying category. In retrospect, one can first construct syntactically the classifying category of a monoidal algebraic theory T and then use information on this to obtain factorisation theorems; however, factorisation theorems obtained in this form are not as sharp as those proved in the previous sections.

References

[1] F.A.A. Al-Agl, R. Brown, R. Steiner, Multiple categories: the equivalence of a globular and a cubical approach, Adv. Math. 170 (2002), 71–118.

[2] J.M. Boardmann, R.M. Vogt, Homotopy invariant algebraic structures on topological spaces, Lecture Notes in Mathematics vol. 347, Springer 1973.

[3] R. Brown, A. Heyworth, Using rewriting systems to compute left Kan extensions and induced actions of categories, J Symbolic Computation 29 (2000), 5–31.

210  MARCO GRANDIS AND LUCA MAURI

[4] R. Brown, P.J. Higgins, On the algebra of cubes, J. Pure Appl. Algebra 21 (1981), 233–260.

[5] R. Brown, P.J. Higgins, Colimit theorems for relative homotopy groups, J. Pure Appl. Algebra 22 (1981), 11–41.

[6] R. Brown, P.J. Higgins, Tensor products and homotopies for ω-groupoids and crossed complexes, J. Pure Appl. Algebra 47 (1987), 1–33.

[7] H.S.M. Coxeter, W.O.J. Moser, Generators and relations for discrete groups, Springer 1957.

[8] S.E. Crans, On combinatorial models for higher dimensional homotopies, Thesis, University of Utrecht, NL (1995).

[9] Roy L. Crole, Categories for types, Cambridge University Press 1993.

[10] E.B. Curtis, Simplicial homotopy theory, Adv. Math. 6 (1971) 107-209.

[11] N. Dershowitz, J.P. Jouannaud, Rewrite systems. in: Handbook of theoretical computer science, Vol. B, Elsevier, Amsterdam 1990, pp. 243–320.

[12] P. Gaucher, Homotopy invariants of higher dimensional categories and concurrency in computer science, Math. Struct. in Comp. Science 10 (2000), 481–524.

[13] P.G. Goerss, J.F. Jardine, Simplicial homotopy theory, Birkhäuser 1999.

[14] M. Grandis, Cubical monads and their symmetries, in: Proc. of the Eleventh Intern. Conf. on Topology, Trieste 1993, Rend. Ist. Mat. Univ. Trieste 25 (1993), 223-262.

[15] M. Grandis, Categorically algebraic foundations for homotopical algebra, Appl. Categ. Structures 5 (1997), 363–413.

[16] M. Grandis, On the homotopy structure of strongly homotopy associative algebras, J. Pure Appl. Algebra 134 (1999), 15–81.

[17] M. Grandis, Finite sets and symmetric simplicial sets, Theory Appl. Categ. 8 (2001), No. 8, 244–252 (electronic). http://tac.mta.ca/tac/

[18] M. Grandis, Higher fundamental functors for simplicial sets, Cahiers Topologie Geom. Differentielle Categ., 42 (2001), 101–136.

[19] G. Huet, Confluent reductions: abstract properties and applications to term rewriting systems, J. Assoc. Comput. Mach. 27 (1980), 797–821.

[20] B. Jacobs, Categorical logic and type theory, North Holland 1999.

[21] C. B. Jay, Languages for monoidal categories, J. Pure Appl. Algebra 59 (1989) 61–85.

[22] D.L. Johnson, Topics in the theory of presentation of groups, Cambridge University Press 1980.

[23] G.M. Kelly, Basic concepts of enriched category theory, Cambridge University Press 1982.

[24] A. Joyal, R. Street, Braided tensor categories, Adv. Math. 102 (1993), 20–78.

[25] A. Kock, G. Reyes, Doctrines in categorical logic, In: J. Barwise (editor), Handbook of mathematical logic, North Holland 1977.

[26] S. Mac Lane, Categorical algebra, Bull. Amer. Math. Soc. 71 (1965), 40–106.

[27] S. Mac Lane, Categories for the working mathematician, Springer 1971.

[28] W. Massey, Singular homology theory, Springer 1980.

[29] L. Mauri, Algebraic theories in monoidal categories, in preparation.

[30] J.P. May, Simplicial objects in algebraic topology, Van Nostrand 1967.

[31] Rotman, The theory of groups, Allyn and Bacon 1973.

[32] R. Street, The petit topos of globular sets, J. Pure Appl. Algebra 154 (2000), 299–315.

[33] A.P. Tonks, Cubical groups which are Kan, J. Pure Appl. Algebra 81 (1992), 83–87.

Dipartimento di Matematica Università di Genova Via Dodecaneso 35 16146-Genova, Italy

Institut für Mathematik Universität Duisburg-Essen Lotharstrasse 65 47048 Duisburg, Germany

Email: grandis@dima.unige.it
      mauri@math.uni-duisburg.de

This article may be accessed via WWW at http://www.tac.mta.ca/tac/ or by anony-

mous ftp at ftp://ftp.tac.mta.ca/pub/tac/html/volumes/11/8/11-08.{dvi,ps}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods.

Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication.

The method of distribution of the journal is via the Internet tools WWW/ftp. The journal is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi, Postscript and PDF. Details will be e-mailed to new subscribers. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh,

rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX is the preferred flavour. TEX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. They are listed below. Please obtain detailed information on submission format and style files from the journal’s WWW server at http://www.tac.mta.ca/tac/. You may also write to tac@mta.ca to receive details by e-mail.

Editorial board.

John Baez, University of California, Riverside: baez@math.ucr.edu Michael Barr, McGill University: barr@barrs.org, Associate Managing Editor Lawrence Breen, Université Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of Wales Bangor: r.brown@bangor.ac.uk Jean-Luc Brylinski, Pennsylvania State University: jlb@math.psu.edu Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Palo Alto Research Center: paiva@parc.xerox.com Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk G. Max Kelly, University of Sydney: maxk@maths.usyd.edu.au Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca, Managing Editor Jiri Rosicky, Masaryk University: rosicky@math.muni.cz James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca