Coalgebras are categorical presentations of state-based systems. In investigating parallel composition of coalgebras (realizing concurrency), we observe 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 microcosm 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.
|Title of host publication||Foundations of Software Science and Computational Structures (Proceedings 11th International Conference, FoSSaCS 2008, Budapest, Hungary, March 29-April 6, 2008)|
|Place of Publication||Berlin|
|Publication status||Published - 2008|
|Name||Lecture Notes in Computer Science|