Ichiro Hasuo 1,3,4 , Bart Jacobs 1,*, and Ana Sokolova 2,** 1 Radboud University Nijmegen, the Netherlands ²  University of Salzburg, Austria ³  RIMS, Kyoto University, Japan 4  PRESTO Research Promotion Program, Japan Science and Technology Agency Abstract.  Coalgebras are categorical presentations of state-based systems. In in- vestigating parallel composition of coalgebras (realizing concurrency) , we ob- serve that the same algebraic theory is interpreted in two different domains in a nested manner, namely: in the category of coalgebras, and in the final coalgebra as an object in it. This phenomenon is what Baez and Dolan have called the mi- crocosm principle , a prototypical example of which is "a monoid in a monoidal category." In this paper we obtain a formalization of the microcosm principle in which such a nested model is expressed categorically as a suitable lax natural transformation. An application of this account is a general compositionality result which supports modular verification of complex systems.
1
Introduction
Design of systems with concurrency is nowadays one of the mainstream challenges in computer science [19]. Concurrency is everywhere: with the Internet being the biggest example and multi-core processors the smallest; also in a modular, component-based architecture of a complex system its components collaborate in a concurrent manner. However, numerous difficulties have been identified in getting concurrency right. For example, a system's exponentially growing complexity is one of the main obstacles. One way to cope with it is a modular verification method in which correctness of the whole system C 1  ‖| · ·· ‖| C n is established using correctness of each component C i . Compositionality —meaning that the behavior of C || D is determined by the behavior of C and that of D —is an essential property for such a modular method to work. Coalgebras as s systems  This paper is a starting point of our research program aimed at better understanding of the mathematical nature of concurrency. In its course we shall use coalgebras as presentations of systems to be run in parallel. The use of coalgebras as an appropriate abstract model of state-based systems is increasingly established [11,26]; the notion's mathematical simplicity and clarity provide us with a sound foundation
for our exploration. The following table summarizes how ingredients of the theory of systems are presented as coalgebraic constructs. This view of "coalgebras as systems" has been successfully applied in the category Sets of sets and functions, in which case the word "behavior" in (1) refers (roughly) to bisimilarity. Our recent work [5,6] has shown that "behavior" can also refer to trace semantics by moving from Sets to a suitable Kleisli category. Compositionality in coalgebras  We start with the following question: what is "com- positionality" in this coalgebraic setting? Conventionally compositionality is expressed as: C  ～ C ′ and D  ～ D ′ implies C ||  D  ～ C ′ ||  D ′ , where the relation  ～ denotes the behavioral equivalence of interest. If this is the case the relation 〜 is s aid to be a congruence , with its oft-heard instance being "bisimilarity is a congruence." When we interpret "behavior" in compositionality as the coalgebraic behavior in- duced by coinduction (see (1)), the following equation comes natural as a coalgebraic presentation of compositionality.
But a closer look reveals that the two "parallel composition operators" || in the equation have in fact different types: the first one Coalg F × Coalg F → Coalg F combines systems (as coalgebras) and the second one Z × Z → Z combines behavior (as states of the final coalgebra). 5 Moreover, the two domains are actually nested: the latter one Z ⇒ FZ is an object of the former one Coalg F. The microcosm principle  What we have just observed is one instance—probably the first one explicitly claimed in computer science—of the microcosm principle as it is called by Baez and Dolan [1]. It refers to a phenomenon that the same algebraic theory (or algebraic "specification," consisting of operations and equations) is interpreted twice in a nested manner, once in a category C and the other time in its object X ∈ C. This is not something very unusual, because "a monoid in a monoidal category" constitutes
Notice here that the outer operation ® appears in the formulation of the inner operation μ . Moreover, to be precise, in the inner "equations" the outer isomorphisms should be present in suitable places. Hence this monoid example demonstrates that, in such nested algebraic structures, the inner structure depends on the outer. What is a mathematically precise formalization of such nested models? Answering this question is a main goal of this paper. Such a formalization has been done in [1] when algebraic structures are specified in the form of opetopes . Here instead we shall formalize the microcosm principle for Lawvere theories [18], whose role as categorical representation of algebraic theories has been recognized in theoretical computer science. As it t urns out, our formalization looks like the situation on the right. Here L is a category (a Lawvere theory) representing an alge- braic theory; an outer model C is a product-preserving functor; and CAT an inner model X is a lax natural transformation. The whole setting is 2-categorical: 2-categories (categories in categories) serve as an appropriate basis for the microcosm principle (algebras in algebras). Applications to coalgebras: parallel composition via sync  The categorical account we have sketched above shall be applied to our original question about parallel com- position of coalgebras. As a main application we prove a generic compositionality the- orem . For an arbitrary algebraic theory L, compositionality like (2) is formulated as follows: the "behavior" functor beh : Coalg F  → C/Z via coinduction preserves an L -structure. This general form of compositionality holds if: C has an L -structure and F : C → C lax-preserves the IL-structure. Turning back to the original setting of (2), these general assumptions read roughly as follows: the base category C has a binary operation || ; and the endofunctor F comes with a natural transformation sync : FX ‖ FY → F(X ‖ Y). Essentially, this sync is what lifts || on C to || on Coalg F , hence "parallel composition via sync." It is called a synchronization because it specifies the way two systems synchronize with each other. In fact, for a fixed functor F there can be different choices of sync (such as CSP-style vs. CCS-style), which in turn yield different "parallel composition" operators on the category Coalg F Related work  Our interest is pretty similar to that of studies of bialgebraic structures in computer science (such as [3,12,14–16,27]), in the sense that we are also concerned (3) about algebraic structures on coalgebras as systems. Our current framework is distin- guished in the following aspects. First, we handle equations in an algebraic theory as an integral part of our ap- proach. Equations such as associativity and commutativity appear explicitly as com- mutative diagrams in a Lawvere theory L. We benefit from this explicitness in e.g. spelling out a condition for the generic associativity result (Theorem 2.4). In contrast, in the bialgebraic studies an algebraic theory is presented either by an endofunctor X  →  [[ σ ∈ Σ , X | σ | or by a monad T . In the former case equations are simply not present; in the latter case equations are there but only implicitly. Secondly and more importantly, by considering higher-dimensional, nested alge- braic structures, we can now compose different coalgebras as well as different states of the same coalgebra. In this way the current work can be seen as a higher-dimensional extension of the existing bialgebraic studies (which focus on "inner" algebraic struc- tures). Organization of the paper  We shall not dive into our 2-categorical exploration from the beginning. In Section 2, we instead focus on one specific algebraic theory, namely the one for parallel composition of systems. Our emphasis there is on the fact that the sync natural transformation essentially gives rise to parallel composition ||, and the fact that equational properties of || (such as associativity) can be reduced to the corresponding equational properties of sync. These concrete observations will provide us with intuition for abstract categorical constructs in Section 3, where we formalize the microcosm principle for an arbitrary Lawvere theory L. Results on coalgebras such as compositionality are proved here in their full generality and abstraction. In this paper we shall focus on strict algebraic structures on categories in order to avoid complicated coherence issues. This means for example that we only consider strict monoidal categories for which the isomorphisms in (3) are in fact equalities. How- ever, we have also obtained some preliminary observations on relaxed ("pseudo" or "strong"') algebraic structures: see Section 3.3.
2
Parallel composition of coalgebras
2.1  Parallel composition via sync natural transformation
Let us s start with the equation (2), a coalgebraic representation of compositionality. The operator ‖| on the left is of type Coalg F × Coalg F → Coalg F . It is natural to re- quire functoriality of this operation, making it a bifunctor . A bifunctor—especially an associative one which we investigate in Section 2.3—plays an important role in various applications of category theory. Usually such an (associative) bifunctor is called a tensor and denoted by &, a convention that we also follow. Therefore the "compositionality" statement now looks as follows.
The first question is: when do we have such a tensor & on Coalg F ? In many appli- cations of coalgebras, it is obtained by lifting a tensor ® on the base category C to Coalg F .6 Such a lifting is possible in presence of a natural transformation
We shall cal this sync a synchronization because its computational meaning is indeed a specification of the way two systems synchronize. This will be illustrated in the coming examples. Once we have an outer parallel composition ®, an inner operator || which composes behavior (i.e. states of the final coalgebra) is also obtained immediately by coinduction as on the right. Compositionality (4) is also straightforward by finality: both sides of the equation are the unique coalgebra morphism from c S d to the final ζ . The following theorem summarizes the observations so far. Theorem 2.1 (Coalgebraic compositionality)  Assume that a category C has a tensor B  :  C × C  →  C  and an endofunctor F  :  C  →  C has a natural transformation sync χ y : F X ® FY → F ( X ® Y ). If moreover there exists a final F -coalgebra, then: 1. The tensor ® on C lifts to an “outer” composition operator ® : Coalg F × Coalgr → Coalgr. 2. We obtain an “inner” composition operator ||: Z ® Z → Z by coinduction. 3. Between the two composition operators the compositionality property (4) holds. □ We can put the compositionality property (4) in more abstract terms as "the functor beh : Coalg F  → C/Z preserves a tensor," meaning that the diagram below left com- mutes. Here a tensor ® on the slice category C/Z is given as on the right, using the inner composition ||.
The point of Theorem 2.1 is as follows. Those parallel composition operators which are induced by sync are well-behaved ones: good properties like compositionality come for free. We shall present some examples in Section 2.2. Remark 2.2 The view of parallel composition of systems as a tensor structure on Coalg F has been previously presented in [13]. The interest there is on categorical structures on Coalg r rather than on properties of parallel composition such as compo- sitionality. In [13] and other literature an endofunctor F with sync (equipped with some additional compatibility) is called a monoidal endofunctor. 7
2.2  Examples
In Sets: bisimilarity is a congruence  We shall focus on LTSs and bisimilarity as their process semantics. For this purpose it is appropriate to take Sets as our base category C and P ω (Σ × _ ) as the functor F . We use Cartesian products as a tensor on Sets. This means that a composition of two coalgebras has the product of the two state spaces as its state space, which matches our intuition. The functor P ω in F is the finite powerset functor; the finiteness assumption is needed for existence of a final F -coalgebra. It is standard (see e.g. [26]) that a final F -coalgebra captures bisimilarity via coinduction. In considering parallel composition of LTSs, the following two examples are well- known ones. 8 – CSP-style [7]: a.P || a.Q  ⇒ P  || Q. For the whole system to make an a -action, each component has to make an a-action. – CCS-style [21]: a.P || ä.Q  → P || Q, assuming Σ = {a,b,...}∪{ä,b,...}∪{ｧ}. When one component outputs on a channel a and another inputs from a , then the whole system makes an internal τ move. In fact, each of these different ways of synchronization can be represented by a suitable sync natural transformation.
By Theorem 2.1, each of these gives (different) & on Coalg F , and ‖ on Z ; moreover the behavior functor beh satisfies compositionality. In other words: bisimilarity is a congruence with respect to both CSP-style and CCS-style parallel composition. Remark 2.3  As mentioned in the introduction, in some ways this paper can be seen as an extension of the bialgebraic studies started in [27]. However there is also a drawback, namely the limited expressive power of sync : FX ® FY → F(X ® Y). Our sync specifies the way an algebraic structure interacts with a coalgebraic one. In this sense it is a counterpart of a distributive law ΣF ⇒ FΣ in [27] representing operational rules, where Σ is a functor induced by an algebraic signature. However there are many common operational rules which do not allow representation of the form ΣF ⇒ FΣ ; therefore in [27] the type of such a distributive law is eventually extended to Σ(F × id) ⇒ F Σ *. The class of rules representable in this form coincides with the class of so-called GSOS-rules. At present it is not clear how we can make a similar extension for our sync; conse- quently there are some operational rules which we cannot model by sync. One impor- tant example is an interleaving kind of interaction—such as a.P ‖ Q ⇒ P ‖ Q which leaves the second component unchanged. This is taken care of in [27] by the identity functor (id) appearing on the left-hand side of Σ(F × id) ⇒ FΣ*. For our sync to be able to model such interleaving, we can replace F by the cofree comonad on it, as is done in [13, Example 3.11]. This extension should be straightforward but detailed treatment is left as future work. In Kl(T): trace equivalence is a congruence  In our recent work [6] we extend earlier observations in [10,25] and show that trace semantics—including trace set se- mantics for non-deterministic systems and trace distribution semantics for probabilistic systems—is also captured by coinduction when it is employed in a Kleisli category K ℓ( T ). Applying the present composition framework, we can conclude that trace se- mantics is compositional with respect to well-behaved parallel composition. The details are omitted here due to lack of space.
Equational properties of parallel composition
2.3
Now we shall investigate equational properties—associativity, commutativity, and so on—of parallel composition ®, which we have ignored deliberately for simplicity of argument. We present our result in terms of associativity; it is straightforward to trans- fer the result to other properties like commutativity. The main point of the following theorem is as follows: if ® is associative and sync is "associative," then the lifting ® is associative. The proof is straightforward. Theorem 2.4  Let C be a category with a strictly associative tensor ®, 9 and F : C → C be a functor with sync : FX ® FY → F(X ® Y). If the diagram
commutes, then the lifted tensor ® on Coalg F is strictly associative.
The two identity arrows in (7) are available due to strict associativity of *. In the next section we shall reveal the generic principle behind the commutativity condition of (7), namely a coherence condition on a lax natural transformation. As an example, sync SP and sync CCS in Section 2.2 are easily seen to be "asso- ciative" in the sense of the diagram (7). Therefore the resulting tensors ® are strictly associative.
Formalizing the microcosm principle
3
In this section we shall formalize the microcosm principle for an arbitrary algebraic theory presented as a Lawvere theory L. This and the subsequent results generalize the results in the previous section. In particular, we will obtain a general compositionality result which works for an arbitrary algebraic theory. As we sketched in the introduction, an outer model will be a product-preserving functor C : L → CAT; an inner model inside will be a lax natural transformation X : 1 ⇒ C. Here 1 : L → CAT CAT is the constant functor which maps everything to the category 1 with one object and one arrow (which is a special case of an outer model). Mediating 2-cells for the lax natural transformation X play a crucial role as inner interpretation of alge- braic operations. In this section we heavily rely on 2-categorical notions, about which detailed accounts can be found in [4].
3.1  Lawvere theories
Lawvere theories are categorical presentations of algebraic theories. The notion is intro- duced in [18] (not under this name, though) aiming at a categorical formulation of "the- ories" and "semantics." An accessible introduction to the notion can be found in [17]. Lawvere theories are known to be equivalent to finitary monads . These two ways of presenting algebraic theories have been widely used in theoretical computer science, e.g. for modeling computation with effect [8,22]. Recent developments (such as [24]) utilize the increased expressive power of enriched Lawvere theories. In the sequel, by an FP-category we refer to a category with (a choice of) finite prod- ucts. An FP-functor is a functor between FP-categories which preserves finite products "on-the-nose," that is, up-to-equality instead of up-to-isomorphism. Definition 3.1 (Lawvere theory)  By Nat we denote the category of natural numbers (as sets) and functions between them. Therefore every arrow in Nat is a (cotuple of) coprojection; an arrow in Nat op is a (tuple of) projection. 10 A Lawvere theory is a small FP-category L equipped with an FP-functor H  : Nat op → L which is bijective on objects. We shall denote an object of L by a natu- ral number k , identifying k ∈ Nat°P and Hk ∈ L. The category Nat op — which is a free FP-category on the trivial category 1 — is there in order to specify the choice of f inite products in L. For illustration, we make some remarks on L’s objects and arrows. − An object k ∈ L is a k -fold product 1 × ･ · × 1 of 1. − An arrow in L is intuitively understood as an algebraic operation. That is, k → 1 as a k -ary operation; and k → n as an n -tuple ⟨ f 1 , . . , f n ⟩ of k -ary operations. To be precise, arrows in L also include projections (such as π 1 : 2 → 1) and terms made up of operations and projections (such as m o (π1,π2): 3 → 1). Conventionally in universal algebra, an algebraic theory is presented by an algebraic specification ( Σ , E ) —a pair of a set Σ of operations and a set E of equations. A Law- vere theory L arises from such ( Σ , E ) as its so-called classifying category (see ee.g. [9, 18]). An arrow k  → n in the resulting Lawvere theory L is an n -tuple ([ t 1 ( x )], . . , [ n ( x )]) of Σ -terms with k variables  x , where [_] denotes taking an equivalence class modulo equations in E . An equivalent way to describe this construction is via sketches : ( Σ , Ε ) is identified with an FP-sketch, which in turn induces L as a free FP-category. See [2] for details. Our leading example is the Lawvere theory Mon for monoids. 11 It arises as a classi- fying category from the well-known algebraic specification of monoids. This specifica- tion has a nullary operation e and a binary one m; subject to the equations m(x, e) = x, m(e, x) = x, and m(x, m(y, z)) = m(m(x,y), z). Equivalently, Mon is the freely generated FP- category by arrows (  ⇒  1 and 2  ⇒  1 subject to the commutativity on the right. These data (arrows and com- mutative diagrams) form an FP-sketch (see [2]).
3.2    Outer models: L-categories
We start by formalizing an outer model. It is a category with an L-structure, hence called an IL-category . It is standard that a (set- theoretic) model of IL —a set with an L-structure—is identified with an FP-functor L ☭ Sets. Concretely, let X  =  X1 be the image of 1 ∈ L. Then k ∈ L must be sent to X k due to preservation of finite products. Now the functor's action on arrows is what interprets L's operations in X , as illustrated above right. Equations (expressed as commutative diagrams in L ) are satisfied because a func- tor preserves commutativity. Turning back to L-categories , what we have to do here is to just replace Sets by the category CAT of (possibly large and locally small) categories. Definition 3.2 ( L-categories, L-functors)  A (strict) L-category is an FP-functor L   → CAT. In the sequel we denote the image C1 of 1 ∈ L by C; and the image C(f) of an arrow f by [f]. An L -functor F : C → D —a functor preserving an L -structure—is a natural trans- formation  L    # Another way to look at the previous definition is to view an L-structure as "factor- ization through Nat ° P  →  L." We can identify a category C  ∈  CAT with a functor 1 → CAT, which is in turn identified with an FP-functor Nat op  → CAT, because Nat oP is the free FP-category on 1. We say that C has an L-structure, if this FP- functor factors through H : Nat oP → L (as below left). Note that the factorization is not necessarily unique, because there can be different ways of interpreting the algebraic theory L in C. Similarly, a functor C  ⇒ D is identified with a natural transforma- tion  1   TF   CAT  ; and then with  Nat oP    $F   CAT  due to the 2-universality of Nat oP as a free object. We say that this F preserves an L-structure, if the last natural transformation factors through H : Nat oP → L (as below right).
Example 3.3  The usual notion of strictly monoidal categories coincides with L-categories for L = Mon. A tensor & and a unit I on a category arise as interpretation of the oper- ations 2 〓 1 and 0 → 1; commuting diagrams in Mon such as m o (id, e) = id yield equational properties of ✉ and I .
Remarks on “pseudo” algebraic structures
3.3
As we mentioned in the introduction, in this paper we focus on strict algebraic struc- tures. This means that monoidal categories (in which associativity holds only up-to- isomorphism, for example) fall out of our consideration. Extending our current frame- work to such "pseudo" algebraic structures is one important direction of our future work. Such an extension is not entirely obvious; we shall sketch some preliminary ob- servations in this direction. The starting point is to relax the definition of L-categories from (strict) functors L → CAT to pseudo functors, meaning that composition and identities are preserved only up-to-isomorphism. Then it is not hard to see that a pseudo functor Mon  ⇒ CAT (which preserves finite products in a suitable sense) gives rise to a monoidal category. Indeed, let us denote a mediating iso-2-cell for composition by C g,f : [[g]] o [f]] file lig c f]]. The associativity diagram (below left) gives rise to the two iso-2-cells on the right.
The composition C m,idxm ● Cm,mxid is what gives us a natural isomorphism α : X ® (Y ® Z) ⇒ (X ® Y) ® Z. Moreover, the coherence condition on such isomorphisms in a monoidal category (like the famous pentagon diagram; see [20]) follows from the coherence condition on mediating 2-cells of a pseudo functor (see [4]). So far so good. However, at this moment it is not clear what is a canonical con- struction the other way round, i.e. from a monoidal category to a pseudo functor. 12 In the present paper we side-step these 2-categorical subtleties by restricting ourselves to strict, non-pseudo functors.
3.4    Inner models: L-objects
We proceed to formalize an inner model. It is an object in an L-category which it- self carries an (inner) L-structure, hence is called an L-object . A monoid object in a monoidal category is a prototypical example. We first present an abstract definition; some illustration follows afterwards. Definition 3.4 ( L-objects) An L-object X in an L-category C is a lax natural trans- formation X : 1 ⇒ C (below left) which is "product-preserving": this means that the composition X  。 H (below right) is strictly, non-lax natural. Here 1 : L → CAT denotes the constant functor to the trivial one-object category 1. Such a nested algebraic structure—formalized as an L-object in an L-category—shall be called a microcosm model for L. Let us now illustrate the definition. First, X’s in Natop in C component at 1 ∈ L is a functor 1 ✉⇒ C which is identified with an object X  ∈ C. This is the "car- rier" object of this inner algebra. Moreover, any other component 1 × C k must be the k -tuple ( X , . . , X ) ∈ C k of X ’s. This is be- cause of (strict) naturality of X ㅇH (see above right): for any i ∈ [1, k] the composite π ε ○ X  is required to be X 1 . The (inner) algebraic structure on X arises in the in CA1 in L form of mediating 2-cells of the lax natural trans- formation. For each arrow k  f  n  in L, lax natu- rality of X requires existence of a mediating 2-cell X f : [[f] o X k ⇒ X n . The diagram (above right) shows the situation when we set f == m, a binary operation. The natural transformation X m can be identified with an arrow X ® X    → X in C, which gives an inner binary operation on X . How do such inner operations on X satisfy equations as specified in IL? The key is the coherence condition 13 on medi- ating 2-cells: it requires X id = id concerning identities; and Xgof = Xg ● ([g]] ○ Xf) concerning composition (as on the right). The following example illustrates how such coherence induces equational properties. Example 3.5  A monoid object in a strictly monoidal category is an example of an L- object in an L-category. Here we take L = Mon, the theory of monoids. For illustration, let us here derive associativity of multiplication X ® X   ±  X . In the current setting the multiplication μ is identified with a mediating 2-cell X m as above. The coherence condition yields the two equalities (*) below. Now it is not hard to see that: the composed 2-cell on the left corresponds to X X 2̸≡ X ; and the one on the right corresponds to X 3 µ× X  X 2 µ X .  The equalities (*) above prove that these two arrows X 3 ⇒ X are identical.
3.5
Microcosm structures in coalgebras
In this section we return to our original question and apply the framework we just introduced to coalgebraic settings. First we present some basic results, which are used later in our main result of general compositionality. The constructs in Section 2 (such as sync) will appear again, now in their generalized form. Some details and proofs are omitted here due to lack of space. They will appear in the forthcoming extended version of this paper, although the diligent reader will readily work them out. Let C be an L-category, and F : C → C be a functor. We can imagine that, for the category Coalg F to carry an L -structure, F needs to be somehow compatible with L ; it t urns out that the following condition is sufficient. It is weaker than F "s being an L-functor (see Definition 3.2). Definition 3.6 (Lax L-functor)  A functor F : C → D between L-categories is said to be a lax L-functor if it is identified with 14 some lax natural transformation  L which is product-preserving (i.e. F o H is strictly natural; see Definition 3.4). Lax L-endofunctors are natural generalization of func- in L in CA1 tors with sync as in Section 2. To illustrate this, look at the lax naturality diagram on the right for a binary op- eration m. Here we denote the outer interpretation [[m] by ® . The 2-component is F 2 = ( F , F ) because the lax natural transformation F is product-preserving. The mediating 2-cell F m can be identified with a natural transfor- mation FX ® FY → F(X ® Y) ; this is what we previously called sync. Moreover, F m (as generalized sync) is automatically compatible with equational properties (as in The- orem 2.4); this is because of the coherence condition on mediating 2-cells like " F g of is a suitable composition of F g after F ." The following results folow from a more general result concerning the notion of inserters , namely: when G is an oplax L-functor and F is a lax L-functor, then the inserter Ins(G, F) is an IL-category. 14 Meaning: F : C → D is the 1-component of such a lax natural transformation C → D is Proposition 3.7    1. Let C be an L-category and F : C → C be a lax L-functor. Then Coalg F  is an L-category; moreover the forgetful functor Coalg F  ⇒ C is a (strict, non-lax) L-functor. 2. Given a microcosm model X ∈ C for L, the slice category C/X is an L-category; moreover the functor C/X dom, C is an L-functor. Note that Coalg F being an L-category means not only that operations are interpreted in Coalg ; but also that all the equational properties specified in IL are satisfied in Coalg F . Therefore this result generalizes Theorem 2.4. Concretely, an operation f : k → 1 in IL is interpreted in Coalg F and C/X as follows, respectively. Compare these with (5) and (6); these make an essential use of F f and X f which gener- alize sync and || in Section 2, respectively. 1. A lax L-functor preserves L-objects. Hence so does an L-functor. Proposition 3.8 2.  A final object of an L-category C, if it exists, is an L-object. The inner L-structure is induced by finality. □ We can now present our main result. It generalizes Theorem 2.1, hence is a gener- alized version of the "coalgebraic compositionality" equation (4). Theorem 3.9 (General compositionality)  Let C be an L-category and F : C → C be a lax IL-functor. Assume further that ζ : Z  ⇒ F Z is the final coalgebra. Then the functor beh : Coalg F → C/Z is a (non-lax) L-functor. It makes the following diagram of L-functors commute.
The proof is straightforward by finality. Here Coalg r  is an L-category (Proposition 3.7.1). So is C/Z because: ζ ∈ Coalg F is an L-object (Proposition 3.8.2); Z = Uζ is an L- object (Propositions 3.8.1 and 3.7.1); hence C/Z is an L -category (Proposition 3.7.2). We have also observed some facts which look interesting but are not directly needed for our main result (Theorem 3.9). They include: the category L-obj c  of L-objects in C and morphisms between them forms the lax limit of a diagram C : L → CAT ; the sim- plicial category △ is the "universal" microcosm model for Mon (cf. [20, Proposition VII.5.1]). The details will appear in the forthcoming extended version.
Conclusions and future work
In this paper we have observed that the microcosm principle (as called by Baez and Dolan) brings new mathematical insights into computer science. Specifically, we have looked into parallel composition of coalgebras, which would serve as a mathematical basis for the study of concurrency. As a purely mathematical expedition, we have pre- sented a 2-categorical formalization of the microcosm principle, where an algebraic theory is presented by a Lawvere theory. Turning back to our original motivation, the formalization was applied to coalgebras and yielded some general results which ensure compositionality and equational properties such as associativity. There are many questions yet to be answered. Some of them have been already mentioned, namely: extending the expressive power of sync (Remark 2.3), and a proper treatment of "pseudo" algebraic structures (Section 3.3). On the application side, one direction of future work is to establish a relationship between sync and (syntactic) formats for process algebras. Our sync represents a certain class of operational rules; formats are a more syntactic way to do the same. Formats which guarantee certain good properties (such as commutativity, see [23]) have been actively studied. Such a format should be obtained by translating e.g. a "commutative" sync into a format. On the mathematical side, one direction is to identify more instances of the micro- cosm principle. Mathematics abounds with the (often implicit) idea of nested algebraic structures. To name a few: a topological space in a topos which is itself a "generalized topological space"; a category of domains which itself carries a "structure as a do- main." We wish to turn such an informal statement into a mathematically rigorous one, by generalizing the current formalization of the microcosm principle. As a possible first step towards this direction, we are working on formalizing the microcosm principle for finitary monads which are known to be roughly the same thing as Lawvere theories. Another direction is a search for n -folded nested algebraic structures. In the current paper we have concentrated on two levels of interpretation; an example with more levels might be found e.g. in an internal category in an internal category. Acknowledgments  Thanks are due to Kazuyuki Asada, John Baez, Masahito Hasegawa, Bill Lawvere, Duško Pavlović, John Power and the participants of CALCO-jnr work- shop 2007 including Alexander Kurz for helpful discussions and comments.