A foundational theory of compositional categorical rewriting theory is presented, based on a collection of fibration-like properties that collectively induce and intrinsically structure the large collection of lemmata used in the proofs of theorems such as concurrency and associativity. The resulting highly generic proofs of these theorems are given. It is noteworthy that the proof of the concurrency theorem takes only a few lines and, while that of associativity remains somewhat longer, it would be unreadably long if written directly in terms of the basic lemmata. In essence, our framework improves the readability and ease of comprehension of these proofs by exposing latent modularity. A curated list of known instances of our framework is used to conclude the paper with a detailed discussion of the conditions under which the Double Pushout and Sesqui-Pushout semantics of graph transformation are compositional.

翻译：本文提出了一种组合范畴重写理论的基础理论，该理论基于一系列类纤维化性质，这些性质共同诱导并内在结构化大量用于证明并发性、结合性等定理的引理。我们给出了这些定理的高度泛化证明。值得注意的是，并发性定理的证明仅需数行，而结合性定理的证明虽稍长，但若直接基于基本引理书写，则会因过于冗长而难以阅读。本质上，我们的框架通过揭示潜在模块性，提升了这些证明的可读性与理解便捷性。最后，我们通过精心筛选的已知框架实例列表，详细讨论了“双推图”与“半推图”图变换语义具有组合性的条件。