{'fraction_non_alphanumeric': 0.05633534455382661, 'fraction_numerical': 0.006351222610352493, 'mean_word_length': 3.9320281910728268, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 10, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Weak n-categories: comparing opetopic foundations

We define the category of tidy symmetric multicategories. We construct for each tidy symmetric multicategory Q a cartesian monad (E_Q,T_Q) and extend this assignation to a functor. We exhibit a relationship between the slice construction on symmetric multicategories, and the `free operad' monad construction on suitable monads. We use this to give an explicit description of the relationship between Baez-Dolan and Leinster opetopes.


Introduction
The problem of defining a weak n-category has been approached in various different ways ( [3], [9], [15], [20], [4], [24], [23], [19], [18]), but so far the relationship between these approaches has not been fully understood. The subject of the present paper is the relationship between the approaches given in [3] and [15]. This work is a continuation of the work of [7], in which we exhibited a relationship between the approaches of [3] and [9]. The effect of the present paper is therefore to establish a relationship between all three approaches. We refer the reader to Section 1 of [7] for an overview of the subject.
In each of the cases in question the definition has two components. First, the language for describing k-cells is set up. Then, a concept of universality is introduced, to deal with composition and coherence. Any comparison of these approaches must therefore begin at the construction of k-cells, and in this paper, as in [7], we restrict our attention to this process. This, in the terminology of Baez and Dolan, is the theory of opetopes.
The idea behind the opetopic approaches is to construct opetopes as the underlying shapes of cells. These are described using the language of multicategories. k-cells are constructed from formal composites or 'pasting diagrams' of (k -1)-cells, so a k-cell is considered as an arrow from a list of its constituent (k -1)-cells to a (k -1)-cell. This raises an immediate question: in what order should we list the constituent (k -1)-cells? As Leinster points out in [15], there is in general no ordering that is stable under composition. The different approaches we consider here arise from, essentially, different ways of dealing with this problem. John Baez and James Dolan tackle the problem by including all possible orderings, giving rise to a symmetric action. In [3], they give a definition of weak n-categories based on operads (symmetric multicategories), opetopes and opetopic sets.
In [9], Claudio Hermida, Michael Makkai and John Power begin an explicitly analogous definition, based on (generalised) multicategories, multitopes and multitopic sets. This version arises from tackling the above problem by choosing one ordering for each cell; the resulting complications are dealt with by generalising the notion of composition.
In [7] the relationship between these approaches is made explicit, as far as the notions of opetopes and multitopes.
First we exhibit an embedding ξ : GenMulticat ֒→ SymMulticat of the category of generalised multicategories into the category of symmetric multicategories. We then examine the slicing process, used for constructing k-cells from (k − 1)-cells, and we show that the functor ξ "commutes" with slicing (up to equivalence). Finally, since opetopes and multitopes arise from iterated slicing, we deduce that the respective categories of k-opetopes and k-multitopes are equivalent. In fact, we do not use the definition of opetopes precisely as given in [3], but rather, we develop a generalisation of the notion along lines which Baez and Dolan began but chose to abandon, for reasons unknown to the present author.
Motivated by this work, in the present paper we continue to use the generalisation of the opetopic approach rather than the approach precisely as given in [3].
In [15], Tom Leinster gives an approach to the construction which is quite different; he tackles the problem of ordering constituent cells by not ordering them at all. Instead of attempting to squash the constituent cells into a line for the purpose of listing them as the source of an arrow, they are allowed to remain in their natural 'positions', and the notion of arrow is generalised instead. So this approach is based on (E, T )-multicategories; these structures were defined by Burroni ([5]) and have also been treated by Hermida ([8]). Here, the source of an arrow is not necessarily given as a list of objects, but as a structure given by some cartesian monad T .
The role that these (even more generalised) multicategories plays is not explicitly analogous to that of operads and multicategories in the opetopic and multitopic versions respectively, so the comparison is more subtle. In fact, rather than comparing the role of symmetric multicategories with that of (E, T )-multicategories, we compare it with the role of cartesian monads. This is the subject of Section 1.3.
To study this relationship, we can restrict our attention to a certain kind of particularly well behaved symmetric multicategory. We call a symmetric multicategory tidy if it is freely symmetric and has a category of objects equivalent to a discrete category. We observe ( [7]) that the multicategories involved in the construction of Baez-Dolan opetopes are all tidy; also, a symmetric multicategory is equivalent to one in the image of ξ if and only if it is tidy. We write TidySymMulticat for the full subcategory of SymMulticat whose objects are tidy symmetric multicategories.
In Section 1.3 we construct a functor where CartMonad is the category of cartesian monads and cartesian monad opfunctors. Roughly, given a tidy symmetric multicategory Q we construct a cartesian monad (E Q , T Q ) which acts on sets of 'labelled Q-objects' to give sets of 'source-labelled Q-arrows'. The idea is that, for an (E, T )-multicategory, much information about an arrow is given by its domain, that is, the action of T ; in the Baez-Dolan setting the domain of an arrow is just a list of objects, and the information is captured elsewhere. So, the functor part of T Q is constructed from the collection of arrows itself, the unit from the identities, and multiplication from the reduction laws of Q.
In Section 2 we examine the construction of opetopes. First we examine the process of constructing k-cells from (k -1)-cells. In [3] Baez and Dolan define the 'slicing' process for this purpose. Leinster does define a slicing process on (E, T )-multicategories, but since we are considering a comparison between symmetric multicategories and monads, we seek an analogous process defined on these monads, rather than on (E, T )-multicategories. This process is the 'free (E, T )-operad monad' construction, defined on suitable monads ( [16]).
Given a suitable monad (E, T ), the monad (E, T ) ′ = (E ′ , T ′ ) is defined to be the free (E, T )-operad monad. We show that In this sense, the processes are analogous.
Finally, we apply these results to the construction of opetopes. Having established a relationship between the underlying theories, it is straightforward to compare these constructions. In the Baez-Dolan setting, the category of k-opetopes is defined to be the object-category of I k+ , where I is the symmetric multicategory with only one object and one (identity) arrow.
Leinster gives a construction of 'opetopes' with a role analogous to that of Baez-Dolan opetopes, based on a series (Set/S n , T n ) of cartesian monads. We show that, for each n ≥ 0 ζ(I n+ ) ∼ = (Set/S n , T n ) and deduce that o(I n+ ) ≃ S n for each n ≥ 0, where o denotes the object-category. Informally, we see that Baez-Dolan opetopes and Leinster opetopes are the same up to isomorphism. Throughout this paper we repeatedly find that the details of proofs are fiddly but uninteresting. So we include some informal comments about how the constructions may be interpreted, as a gesture towards demonstrating that the notions are in fact naturally arising. The aim is to shed some light on the relationship between the various structures involved, a relationship which has previously remained unclear.
Finally, we note that some of the constructions given in [15] and [16] may be treated in slightly greater detail in [17], in particular the free multicategory and slicing constructions.
Terminology i) Since we are concerned chiefly with weak n-categories, we follow Baez and Dolan ( [3]) and omit the word 'weak' unless emphasis is required; we refer to strict n-categories as 'strict n-categories'.
ii) We use the term 'weak n-functor' for an n-functor where functoriality holds up to coherent isomorphisms, and 'lax' functor when the constraints are not necessarily invertible.
iii) In [3] Baez and Dolan use the terms 'operad' and 'types' where we use 'multicategory' and 'objects'; the latter terminology is more consistent with Leinster's use of 'operad' to describe a multicategory whose 'objects-object' is 1.
iv) In [9] Hermida, Makkai and Power use the term 'multitope' for the objects constructed in analogy with the 'opetopes' of [3]. This is intended to reflect the fact that opetopes are constructed using operads but multitopes using multicategories, a distinction that we have removed by using the term 'multicategory' in both cases. However, we continue to use the term 'opetope' and furthermore, use it in general to refer to the analogous objects constructed in each of the three theories. Note also that Leinster uses the term 'opetope' to describe objects which are analogous but not a priori the same; we refer to these as 'Leinster opetopes' if clarification is needed. vi) We regard sets as sets or discrete categories with no notational distinction.

The theory of multicategories
Opetopes are described using the language of multicategories. In each of the three theories of opetopes in question, a different underlying theory of multicategories is used. In this section we examine the underlying theories, and we construct a way of relating these theories to one another; this relationship provides subsequent equivalences between the definitions. We adopt a concrete approach here; certain aspects of the definitions suggest a more abstract approach but this will require further work beyond the scope of this work.

Symmetric multicategories
By 'symmetric multicategory' we mean symmetric multicategory with a category of objects. Such structures are defined (as 'operads') in [3]; see also [7]. We recall the definition here. We write F for the 'free symmetric strict monoidal category' monad on Cat, and S k for the group of permutations on k objects; we also write ι for the identity permutation. Definition 1.1 A symmetric multicategory Q is given by the following data 1) A category o(Q) = C of objects. We refer to C as the object-category, the morphisms of C as object-morphisms, and if C is discrete, we say that Q is object-discrete.
2) For each p ∈ FC op × C, a set Q(p) of arrows. Writing an element f ∈ Q(p) is considered as an arrow with source and target given by and we say f has arity k. We may also write a(Q) for the set of all arrows of Q.

5) For any
where σ ∈ S m 1 +···+m k is the permutation obtained by juxtaposing the σ i .
Definition 1.2 Let Q and R be symmetric multicategories with object-categories C and D respectively. A morphism of symmetric multicategories F : Q −→ R is given by • F preserves symmetric action: Composition of such morphisms is defined in the obvious way, and there is an obvious identity morphism 1 Q : Q −→ Q. Thus symmetric multicategories and their morphisms form a category SymMulticat.
is an equivalence if and only if the functor F 0 : C −→ D is an equivalence, and F is full and faithful. That is, given objects x 1 , . . . , x m , x the induced function is an isomorphism.
Definition 1.4 Let T be a cartesian monad on a cartesian category E. An (E, T )-multicategory is given by an 'objects-object' C 0 and an 'arrows-object' comp −→ C 1 satisfying associative and identity laws. (See [17] for full details.) We write CartMonad for the category of cartesian monads and cartesian monad opfunctors. A cartesian monad opfunctor • a cartesian natural transformation φ : U T 1 −→ T 2 U , that is, a natural transformation whose naturality squares are pullbacks satisfying certain axioms (see [22] and [16] for full definitions).

Relationship between symmetric multicategories and cartesian monads
The respective roles of multicategories in the Baez-Dolan and Leinster approaches are not explicitly analogous. In this section we exhibit instead a correspondence between certain symmetric multicategories and certain cartesian monads, by constructing a functor This is enough since we will see that all the symmetric multicategories involved in the construction of opetopes are tidy.
We begin by defining the action of ζ on objects; so for any tidy symmetric multicategory Q, we construct a cartesian monad ζ(Q) = (E Q , T Q ), say. Informally, the idea behind this construction is that T Q should encapsulate information about the arrows of Q. The functor part is constructed to give the arrows themselves, the unit to give the identities, and multiplication the reduction laws (composites).
Write o(Q) = C. Q is tidy, so C ≃ S, say, where S is a discrete category. For various of the constructions which follow, we assume that we have chosen a specific functor S ∼ −→ C. However, when isomorphism classes are taken subsequently, we observe that the construction in question does not depend on the choice of this functor.
Put E Q = Set/S and observe immediately that this is cartesian. (This is sufficient here, though of course Set/S has much more structure than this.) Informally, an element (X, f ) = (X f −→ S) of Set/S may be thought of as a system for labelling Q-objects with 'compatible' elements of X; each 'label' is compatible with an isomorphism class of Q-objects. Then the action of T Q assigns compatible labels to the source elements of Q-arrows in every way possible; the target is not affected. The resulting set of 'sourcelabelled Q-arrows' is itself made into a set of labels by regarding each arrow as a 'label' for its target.
We now give the formal definition of the functor T Q : where F denotes the free symmetric strict monoidal category monad on Cat, and s and t the source and target functions respectively. Consider the pullback Since Q is tidy, eltQ is equivalent to a discrete category, and so too is the above pullback; so we have We now define the action of T Q on morphisms. A morphism which, by construction, makes the following diagram commute: T Q is clearly functorial; we now show that it inherits a cartesian monad structure from the identities and composition of Q. For convenience we write E Q = E and T Q = T .

• unit
We seek a natural transformation η : 1 E =⇒ T , so with the above notation we need components Given (X, f ) ∈ Set/S, we have a functor X −→ elt Q given by the composite We also have a functor X −→ FX op given by the unit of the monad F. These induce a functor and we define the component η (X,f ) to be the composite Explicitly, η (X,f ) acts as follows. We have So (1 c , x) is an "identity labelled by x", where c ∈ C is any object in the isomorphism class f x. We can see explicitly that this is well defined since if c ∼ = c ′ we have 1 c ∼ = 1 c ′ ∈ eltQ and thus The following diagram commutes Next we show that the components η (X,f ) satisfy naturality; so we show that for any morphism h : (X, f ) −→ (Y, g) ∈ Set/S the following diagram commutes This follows from the construction of η, and naturality of the unit for F; alternatively, we see that on elements, the right-ish leg gives with c in the isomorphism class f x, and the left-ish leg gives It also follows from the construction of η that the square is a pullback; it is similarly easily seen by considering elements.

• multiplication
We seek a natural transformation µ : T 2 =⇒ T . Consider (X, f ) ∈ Set/S. Then by definition We construct a commutative square in Set/S as required. Informally, (X, f ) is a system for labelling Q-objects, and T (X, f ) = (X ′ , f ′ ) gives source-labelled Q-arrows. A typical element of X ′ may be thought of as the isomorphism class of where β i ∈ X ′ and s(α) ∼ = (f ′ (β 1 ), . . . , f ′ (β m )). Writing β i as the isomorphism class of we can draw θ as (the isomorphism class of) where α, α 1 , . . . , α m ∈ eltQ and s(α) ∼ = (t(α 1 ), . . . t(α m )). So, via the relevant object-isomorphisms, we may compose the underlying Q-arrows to give α ′ , say, which is defined up to isomorphism. We then concatenate the X-labels (via the multiplication for F) to give Finally, we take the isomorphism class of this to give µ (X,f ) (θ) ∈ X ′ , and f ′′ (µ (X,f ) (θ)) = [t(α ′ )] = [t(α)] ∈ S. It follows that µ defined in this way is a cartesian natural transformation.

• T preserves pullbacks
First observe that a commutative square in Set/S is a pullback if and only if applying the forgetful functor Set/S −→ Set gives a pullback in Set. Then T preserves pullbacks since F preserves pullbacks.
So T Q = (T, η, µ) is a cartesian monad on E Q = E and we may define ζ(Q) = (E Q , T Q ).
We now define the action of ζ on morphisms. Let F : Q −→ R be a morphism of tidy symmetric multicategories. We construct a cartesian monad opfunctor We define U as follows. On objects, we have a functor giving a morphism on isomorphism classes This induces a functor Set/S Q −→ Set/S R by composition withF , which clearly preserves pullbacks; we define U to be this functor. We now construct the components of φ. Given (X, f ) ∈ Set/S Q write We seek .
The map X Q −→ X R is induced by (F, 1) on isomorphism classes as shown in the diagram, since the pullback is along the morphismF • f . We define φ (X,f ) to be this map. Observe that all squares in the diagram commute, so φ (X,f ) is a morphism in Set/S R as required.
We now check that these components satisfy naturality. Given any morphism h : (X, f ) −→ (Y, g) ∈ Set/S Q , we have the following diagram Considering this componentwise, it clearly commutes and is a pullback. The result on isomorphism classes follows. Finally, by functoriality of F , (U, φ) satisfies the axioms for a monad opfunctor. So (U, φ) is a cartesian monad opfunctor and the construction is clearly functorial. This completes the definition of ζ.
We observe immediately that the construction of (E Q , T Q ) uses only the isomorphism classes of objects and arrows of Q. So Recall (1.1) that we expect that a symmetric multicategory Q may be given as a monad in a certain bicategory, in which case the identities are given by the unit, and composition laws by multiplication. In this abstract framework there should be a morphism from the underlying bicategory to the 2-category Cat, taking the monad Q to the monad T Q , but this is somewhat beyond the scope of this work.

The theory of opetopes
In this section we give the analogous constructions of opetopes in each theory, and show in what sense they are equivalent. That is, we show that the respective categories of k-opetopes are equivalent.
We first discuss the process by which (k + 1)-cells are constructed from k-cells. Recall that, in [3], the 'slice' construction is used, giving for any symmetric multicategory Q the slice multicategory Q + . In [15] the 'free (E, T )-operad' construction is used, giving, for any 'suitable' monad (E, T ), the free (E, T )-operad monad (E ′ , T ′ ).

Slicing a symmetric multicategory
Let Q be a symmetric multicategory with a category C of objects, so Q may be considered as a functor Q : FC op × C −→ Set with certain extra structure. Recall ( [7]) that the slice multicategory Q + is given by: So the category o(Q + ) has as objects pairs (p, g) with p ∈ FC op × C and g ∈ Q(p); a morphism α : Then, given any arrow we have an arrow α(g) = g ′ ∈ Q(y 1 , . . . , y m ; y) given by (see [7]).
• Arrows: Q + (f 1 , . . . , f n ; f ) is given by the set of 'configurations' for composing f 1 , . . . , f n as arrows of Q, to yield f .
such a configuration is given by (T, ρ, τ ) where 1) T is a planar tree with n nodes. Each node is labelled by one of the f i , and each edge is labelled by an object-morphism of Q in such a way that the (unique) node labelled by f i has precisely m i edges going in from above, labelled by a i1 , . . . , a im i ∈ arr(C), and the edge coming out is labelled a i ∈ a(C), where cod(a ij ) = x ij and dom(a i ) = x i .
2) ρ ∈ S k where k is the number of leaves of T . Note that (T, ρ) may be considered as a 'combed tree', that is, a planar tree with a 'twisting' of branches at the top given by ρ.
The arrow resulting from this composition is given by composing the f i according to their positions in T , with the a ij acting as arrows ι(a ij ) of Q, and then applying ρ according to the symmetric action on Q. This construction uniquely determines an arrow (T, ρ, τ ) ∈ Q + (f 1 , . . . , f n ; f ).
2) τ is the bijection which inserts the source of T 2 into that of T 1 at the mth place.
• Identities: given an object-morphism given by a tree with one node, labelled by g, twist σ, and edges labelled by the f i and f as in the example above.

Slicing a (E, T )-multicategory
In [15] the 'free (E, T )-operad' construction is used to construct (k + 1)-cells from k-cells; this gives, for any suitable monad (E, T ), the 'free (E, T )-operad' monad (E, T ) ′ = (E ′ , T ′ ). In order to compare this construction with the Baez-Dolan slice, we examine the monad ζ(Q) ′ . First we must show that ζ(Q) ′ can actually be constructed, that is, that ζ(Q) = (E Q , T Q ) is a suitable monad.
First recall ( [15]) that a cartesian monad (E, T ) is suitable if it satisfies: 1) E has disjoint finite coproducts which are stable under pullback 2) E has colimits of nested sequences; these commute with pullbacks and have monic coprojections 3) T preserves colimits of nested sequences.
Here a nested sequence is a string of composable monics.
Proposition 2.1 Let Q be a tidy symmetric multicategory. Then (E Q , T Q ) is a suitable monad.
Proof. Certainly E Q is a suitable category, and we have already shown that (E Q , T Q ) is cartesian. So it remains to show that T Q preserves colimits of nested sequences. First observe that a morphism h in Set/S is monic if and only if h is monic as a morphism in Set, that is, injective. Given a nested sequence Since Set is suitable, this nested sequence has a colimit A whose coprojections are monics. Then the morphisms f 0 , f 1 , . . . define a cone with vertex S, inducing a unique morphism A f −→ S making everything commute; (A, f ) is then a colimit for the nested sequence in Set/S. So (A, f ) is a colimit for the nested sequence in Set/S exactly when A is a colimit for the nested sequence in Set.
Having made these observations, it is easy to check that T Q preserves such colimits.

Comparison of slice
In this section we compare the slice constructions and make precise the sense in which they correspond to one another. Recall (Section 1.3) that we have defined a functor We now show that this functor 'commutes' with slicing, up to isomorphism (for ζ). Since , the free (E Q , T Q )-operad monad. Also, Q + is tidy since Q is tidy (see [7]), so we can form the monad ζ(Q + ) = (E Q + , T Q + ). For the comparison, we have the following result.
Proposition 2.2 Let Q be a tidy symmetric multicategory. Then in the category CartMonad.
This proof is somewhat technical and we defer it to Appendix A. Informally, the idea is as follows. T Q + takes a set A of 'labels for arrows of Q' and returns the set A 2 of configurations for composing labelled arrows according to their underlying arrows. On the other hand, T ′ Q takes a diagram of the form and forms the free (E Q , T Q ) multicategory on it, with underlying graph . So T ′ Q gives the set A 1 of all formal composites of arrows labelled in A according to the structure of T Q , which is precisely the set of configurations as above.
We immediately deduce the following result, comparing all three processes of slicing.

Corollary 2.3 Let M be a generalised multicategory. Then
We are now ready to compare the different constructions of opetopes, applying the results we have already established. In each case, opetopes are constructed by iterating the slicing process. Note that the 'opetopes' defined in [15] are not a priori the same as those defined in [3]; when a distinction is required we refer to the former as 'Leinster opetopes'.

Opetopes
We recall the definition of opetopes from [3] and [7]. For any symmetric multicategory Q we write Let I be the symmetric multicategory with precisely one object, precisely one (identity) object-morphism, and precisely one (identity) arrow. A kdimensional opetope, or simply k-opetope, is defined in [3] to be an object of I k+ . We write C k = o(I k+ ), the category of k-opetopes.

Leinster opetopes
In [15], k-opetopes are defined by a sequence (Set/S k , T k ) of cartesian monads given by iterating the slice as follows.
For any cartesian monad (E,T) write Put (E 0 , T 0 ) = (Set, id) and for k ≥ 1 put (E k , T k ) = (Set, id) k ′ . It follows that for each k, (E k , T k ) is of the form (Set/S k , T k ) where S 0 = 1 and S k+1 is given by Then Leinster k-opetopes are defined to be the elements of S k ; as above, we will regard S k as a discrete category.

Comparisons of opetopes
We now compare opetopes and Leinster opetopes.
But I has only one arrow, which is unary (the identity), so Then on objects, the above equivalence gives the following result.
Recall ( [7]) that we also have for each k a (discrete) category P k of 'multitopes', the analogous notion as defined in [9]; in [7] we prove that, for each k ≥ 0, P k ≃ C k . So we immediately have the following result, comparing all three theories: This result shows that multitopes, opetopes, and Leinster opetopes are the same, up to isomorphism.
We eventually aim to define a category Opetope of opetopes of all dimensions, whose morphisms are 'face maps' of opetopes; this is the subject of [6].

A Proof of Proposition 2.2
We now give the proof of Proposition 2.2 deferred from Section 2.3. Proposition 2.2. Let Q be a tidy symmetric multicategory. Then in the category CartMonad. Proof.
By abuse of notation, we write elements of both these categories as sets over S ′ , since confusion is unlikely. Consider Then A 2 ≃ eltQ + × FS ′op FA op , and f 2 is given by the composite Informally, since we are here considering S ′ ≃ o(Q + ) = elt (Q), the object (A f −→ S ′ ) may be thought of as a set of labels for arrows of Q. Then A 2 is the set of all possible source-labelled arrows of Q + . Since an arrow of Q + is given by a tree with nodes corresponding to arrows of Q, an element of A 2 may be thought of as such a tree, with nodes labelled by compatible elements of A. Alternatively, it may be thought of as a configuration for composing labelled arrows of Q via object-isomorphisms, where composition is according to the underlying arrows only. f 2 acts by composing the underlying arrows of Q and then taking isomorphism classes.
We now turn our attention to the action of T Q ′ . (For full details of the free multicategory construction we refer the reader to [16].) For convenience we write T Q = T and S Q = S, so we need to form (T, Set/S) ′ = (T ′ , S ′ ).
To construct A 1 , we form the free multicategory on the following graph: Recall we have The graph underlying the free operad is then The construction gives a sequence of graphs Here • is composition in the bicategory of spans, so the composite is given by the pullback and d k+1 is given by the composite This construction gives a nested sequence (C (k) , f (k) ) ∈ Set/S with (C (0) , f (0) ) = (S, 1) and where (by further abuse of notation) we write is then the colimit of this nested sequence. Informally, the sets C (k) may be thought of as k-fold formal composites (or composites of 'depth' at most k). The formula for C (k) says that a composite is either null or is a generating arrow composed with other composites. We aim to show that these formal composites correspond to the formal composites given by the source-labelled arrows of Q + .
We show that A 1 ∼ = A 2 ≃ elt Q + × FS ′op FA op as follows. For each k we exhibit an embedding g k : C (k) ֒→A 2 which makes the following diagram commute Then the colimit induces the map required.
We proceed by induction. Define g 0 : S −→ eltQ + × FS ′op FA op as follows. Let [x] ∈ S denote the isomorphism class of x ∈ o(Q). Given any [x] ∈ S, we have a nullary arrow α x ∈ Q + (· ; 1 x ). Recall that an arrow of Q + may be regarded as a tree with nodes corresponding to the source elements (which are themselves arrows of Q) and edges labelled by object-morphisms of Q.
Then α x ∈ Q + (· ; 1 x ) is given by a tree with no nodes, that is, a single edge labelled by 1 x as shown below.
The source of α is empty, so we can define g 0 by where (α x , ·) ∈ elt Q + × FS ′ op FA op , and observe immediately that as required.
For the induction step, suppose we have constructed g k satisfying the commuting condition; we seek to construct g k+1 : C (k+1) ֒→A 2 satisfying the condition. Consider y ∈ C (k+1) = S ∐ T (C (k) ) × S ′ A.
Here the map T (C (k) ) −→ S ′ is given by T f (k) . Recall that by definition of T , T (C (k) ) is equivalent to the pullback So, an element of T (C (k) ) is an isomorphism class of arrows of Q sourcelabelled by compatible elements of C (k) . We write the pullback as C (k) . Then T f (k) is the map given by the composite Informally, T f (k) removes the labels, leaving only the (isomorphism class of the) underlying arrow of Q. Now we in fact exhibit a full and faithful functor Let ((β, b), a) ∈ C (k) × S ′ A. So β ∈ eltQ, b = b 1 , . . . , b n ∈ F(C (k) ) op and a ∈ A such that [s Q (β)] = (f (k) (b 1 ), . . . , f (k) (b n )) and f (a) = [β]. Informally, we have an arrow β of Q, source-labelled by the b i ∈ C (k) , and a compatible label a ∈ A. We seek a formal composite of labelled arrows, of depth up to k + 1. By induction, we already have for each element of C (k) a formal composite of labelled arrows, of depth up to k. So we aim to form a formal composite of these together with β labelled by a.
By induction we have for each 1 ≤ i ≤ n g k (b i ) = (π i , p i ) ∈ eltQ + × FS ′op FA op .
The commuting condition implies that for each i This gives us a way of constructing a new element of eltQ + from the data given, since each π i can be composed with β at the ith place, via the appropriate object-isomorphism. That is, we form a tree by induction, as shown in the following diagram where τ i is the tree for π i . Each π i has its nodes (that is, source elements) labelled by elements of A; to complete the definition it remains only to 'label' the node corresponding to β. But we have f (a) = [β], that is, a is a compatible label for β. So we let a be the label for β. So we have defined a full and faithful functor inducing, on isomorphism classes, an embedding g k+1 : C (k) ֒→ A 2 as required. We now check the commuting condition. Informally, d k acts by ignoring the labels and composing the underlying arrows of Q, as does µ. Since µ is induced from composition in Q, and t Q + is constructed from composition of a formal composite of arrows of Q, we have f 2 • g k+1 = d k+1 as required. So we have for each k ≥ 0 an embedding g k as required. The g k then induce a map A 1 −→ A 2 . It is straightforward to check that this is surjective; by construction it makes the following diagram commute as required.