Pith. sign in

REVIEW 4 major objections 5 minor 3 cited by

Towards a double operadic theory of systems

T0 review · 4 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper argues that a single structure—the symmetric monoidal loose right module over a double category—captures systems, their interactions, and their maps, with Petri nets, Moore machines, and ODEs as instances.

desk verdict Serious but conditional: a genuinely new double-categorical framework for systems theories, undercut by a deferred key theorem and a swapped-conditions inconsistency in the sketch. read the letter →

arxiv 2505.18329 v2 pith:RUJAQIQI submitted 2025-05-23 math.CT

Sophie Libkind , David Jaz Myers This is my paper · ORCID
classification math.CT MSC 18N10
keywords categoricalsystemstheorydoublecategoriesloosebimodulesoperadsPetrinetsMooremachineswiringdiagramssymmetricmonoidalstructures
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper proposes a single formal setting for categorical systems theory: a module of systems is a symmetric monoidal loose right module over a symmetric monoidal double category of interfaces and interactions. The package records systems as loose maps, interactions as loose maps of the base double category, and maps between systems (with possibly different interfaces) as squares. The paper then shows that several doctrines—port-plugging by gluing along ports, variable sharing, generalized Moore machines, and ODEs in tangent categories—produce such modules pseudo-functorially, and that undirected and directed wiring diagrams arise as free interactions in these doctrines. A sympathetic reader should care because this promises to unify the operadic and process-theoretic strands of the subject and to give uniform recipes for compositional analysis.

What carries the argument

The load-bearing mechanism is the theory of loose bimodules between double categories, presented as labelling double functors into the walking loose arrow $\mathbf{Loose}$. A module of systems is the right-sided version, and the constructions flow through the restriction pseudo-functor $\mathrm{Res} : \mathcal{N}\mathrm{iche} \to \ell\mathcal{B}\mathrm{imod}$, which restricts a loose bimodule along a pair of double functors and, when those functors are symmetric monoidal with companions and conjoints, produces the symmetric monoidal structure on the restricted module. Around this core sit the span and cospan doctrines built from adequate triples, the lens double categories built from cartesian fibrations, and the doctrine formalism itself, which packages the whole construction as a cartesian 2-functor from a 2-category of systems theories to a 2-category of loose right modules.

What would settle it

On the smallest nontrivial niche—the loose hom bimodule of a double category restricted along identity double functors—the restriction pseudo-functor must return the original bimodule up to isomorphism; checking that the unitors and laxators built in Theorem 3.18 are genuine tight isomorphisms there would settle the deferred theorem, and a failure in this minimal case would refute the central machinery and with it every doctrine example.

Watch

Extended reading notes

Core claim

The central claim is that all the data of a systems theory can be organized as a symmetric monoidal loose right module $S : \bullet \to \mathcal{I}$ over a symmetric monoidal double category $\mathcal{I}$. In this reading, objects of $\mathcal{I}$ are interfaces, tight maps are interface maps, loose maps are interactions, squares are interaction maps, and the carrier $\mathrm{Car}(S)$ is a symmetric monoidal category of systems and system maps acted on by the interactions. The paper works out two detailed examples: open Petri nets form a module over cospans of finite sets, so they compose along undirected wiring diagrams by gluing species; and deterministic Moore machines form a module over the double category of lenses, with trajectories appearing as system maps from a timeline machine. Doctrines build these modules from primitive data: spans in lex categories give variable-sharing systems, cospans in rex categories give port-plugging systems, tangencies give generalized Moore machines and open coalgebras, and first-order differential structures give systems of ODEs. Restricting these doctrines to free interactions makes the operads of wiring diagrams appear as free processes.

Load-bearing premise

The central claim rests on the correctness of the restriction pseudo-functor for loose bimodules, whose full proof is deferred to a companion manuscript; every concrete example in the paper is built by composing through that theorem.

Editorial extensions

If this is right

  • Open Petri nets, with maps between nets of different interfaces, form a module over undirected wiring diagrams; this recovers and extends the hypergraph double category of open Petri nets.
  • Generalized Moore machines—deterministic, non-deterministic, and partially observable Markov decision processes—are instances of one open-coalgebra doctrine, with lens composition as interaction and trajectories as maps from a timeline machine.
  • Systems of ordinary differential equations in any tangent category or first-order differential structure form modules over lens double categories, so composing ODEs along directed wiring diagrams is a special case of restricting the ODE doctrine to free interactions.
  • The variable-sharing doctrine formalizes Willems' behavioral approach, Lagrangian correspondences, and graphical regular logic as modules of systems whose interactions are spans.
  • Pseudo-functoriality of the doctrine constructions gives recipes for black-boxing functors between modules of systems, extending the existing recipes for hypergraph categories to lens-based systems such as ODEs and POMDPs.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the restriction theorem holds in full generality, the Yoneda theory sketched in the paper should make behavioral features such as trajectories, steady states, and Lyapunov functions recoverable as representable maps, yielding compositionality theorems uniformly.
  • The conjecture that symmetric monoidal loose right modules over isofibrant double categories are equivalent to algebras for isofibrant double operads with all tensors, if proven, would justify transferring operadic results into this framework and give a cleaner account of free wiring diagrams.
  • A natural extension is to instantiate the open-coalgebra doctrine with other lax monoidal probability or hyperspace monads; the paper's pseudo-functoriality would then produce compositionality theorems for these new automata types automatically.
  • The free-interaction viewpoint suggests a general recipe for decorated wiring diagrams: generate free interaction theories on algebraic theories of function boxes, so delays, labels, or other decorations appear as free processes rather than ad hoc data.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper proposes a 'double operadic theory of systems' in which a systems theory is packaged as a symmetric monoidal loose right module over a symmetric monoidal double category of interfaces and interactions. The main technical vehicle is the 2-category of loose bimodules, defined via double functors into the walking loose arrow, together with collapse and restriction constructions. The central theorems assert that restriction is a cartesian pseudo-functor (Theorem 3.18) and preserves symmetric monoidal and cartesian structure (Theorem 3.23). These results are then used to build doctrines: initial processes, span and cospan doctrines for adequate triples, generalized Moore machines via tangencies, open coalgebras, and restrictions to free interactions. The paper includes worked examples of open Petri nets and Moore machines and argues that wiring diagrams arise as free interactions in these doctrines.

Significance. If the restriction machinery is correct, the paper provides a genuinely unifying formalism for categorical systems theory: it packages systems, their interactions, and maps between systems, and it yields pseudo-functorial constructions that can support black-boxing compositionality theorems. The exposition is detailed, the examples are carefully chosen, and the use of F-sketches to organise the 2-algebraic structure is valuable. The paper also identifies useful new structure, such as the doctrine of generalized Moore machines and the free-interaction restriction procedure. However, the load-bearing results are mostly deferred to an in-preparation companion paper, and the present manuscript appears to contain a swapped companion/conjoint condition in the definition of Niche. The contribution is therefore significant but currently conditional.

major comments (4)
  1. [§3.3.2, Explication 3.17 and Theorem 3.18] Explication 3.17 defines a 1-cell of Niche by requiring f0 to be a companion commuter transformation and f1 to be a conjoint commuter transformation. In Step 2 of the proof of Theorem 3.18, however, Res(a) is defined using the conjoint (f0 e00)< of the f0-component and the companion (f1 e01)> of the f1-component. Lemma 3.22 uses the same convention, requiring the unitors and laxators of F0 to be conjoints and those of F1 to be companions. Thus the two conditions in Explication 3.17 are interchanged relative to the proof and to Lemma 3.22. Since every doctrine in Sections 5-8 is built through Res, this inconsistency is load-bearing and must be corrected before the main constructions can be considered well-typed.
  2. [§3.3.2, Theorems 3.18 and 3.23] The central pseudo-functoriality of restriction is not established in this paper. The proof of Theorem 3.18 is explicitly deferred to the companion manuscript [BCLJ25], which is listed as in preparation, and Theorem 3.23, stating that restriction preserves symmetric monoidal and cartesian structure, is supported only by a short discussion of 'flexible' 2-algebraic structure. These theorems are the engine for all constructions in Sections 5-8, including port-plugging, variable sharing, Moore machines, and ODEs. The manuscript should either provide complete proofs in an appendix or state clearly that all subsequent claims are conditional on the companion manuscript.
  3. [§3.2, Loose bimodules as pseudo-bimodules] The equivalence between the 'double barrels' definition of loose bimodules and pseudo-bimodules is only sketched: the text says that an inspection of El(Loose) reveals an F-sketch for pseudo-bimodules and appeals to a categorified slice/category-of-elements equivalence, without proof. This equivalence underlies the carrier model (Definition 3.13, Proposition 3.14) and the collapse construction (Theorem 3.15). A complete proof or a precise reference to a proof is needed before these constructions can be used.
  4. [§8.2, Definition 8.4 and Lemma 8.7] The admissibility condition in Definition 8.4 says that I sends the transpose of a colaxator to a companion commuter transformation. Lemma 8.7 then constructs a right niche from a restricted systems theory, but the verification that the induced 1-cell satisfies the companion/conjoint conditions required by Niche_r is not shown. Given the inconsistency in Explication 3.17, this step should be checked explicitly once the definition of Niche is corrected.
minor comments (5)
  1. [Definitions 3.7, 3.8, 3.10] Several definitions in Section 3 contain unfinished sentences: Definition 3.7 ends with 'the 2-category of .', Definition 3.8 has 'be a .', and Definition 3.10 has 'whose source is the and thus'. These need to be completed.
  2. [Theorem 3.18, Step 2] There is a typo in the last term of the displayed composite in Step 2: '(f1 e10)>' should presumably be '(f1 e01)>'.
  3. [Theorem 3.18, opening] The proof of Theorem 3.18 begins with two consecutive 'Proof.' paragraphs; one should be removed.
  4. [Observation 6.2 and Section 8 heading] Observation 6.2 repeats 'Span : AdTr -> Dbl' where the second occurrence should refer to the pointed version, and the heading 'Restricting doctines' contains a typo for 'doctrines'.
  5. [Remark 1.2] The paper uses the term 'double operadic' although the formal comparison to double operads is left as a conjecture in Remark 1.2; the text should state this explicitly so that the title is not read as a proven theorem.

Circularity Check

0 steps flagged · score 2.0 of 10

No circular reduction: the framework is definitional and constructive, with the main caveat being a deferred proof in the authors' own companion paper rather than a circular derivation.

full rationale

The paper's derivation chain is definitional and constructive. A module of systems is defined (Definition 4.1) as a symmetric monoidal loose right module, and the doctrines of Sections 5 through 8 produce modules by restricting loose hom bimodules along niches (Theorem 3.18) and then collapsing. No quantity is fitted to data and no output is equal to an input by construction: the Petri net module, Moore machine module, and ODE module are exactly the constructions that the definitions specify. The paper's reliance on the authors' earlier framework papers ([Jaz21], [Mye20], [Mye21]) is for recalled definitions and context, not for an unstated conclusion. The most significant caveat is a proof gap, not circularity: Theorem 3.18 and Theorem 3.23 are load-bearing for the doctrines, but the paper only sketches them and says 'The sketches given here are previews of the complete proofs, which will appear in our forthcoming companion paper [BCLJ25]' (Section 3 introduction) and, in the proof of Theorem 3.18, 'We will only describe the construction itself, foregoing its proof to [BCLJ25]'. Because [BCLJ25] is an in-preparation companion by overlapping authors, this is a deferred-proof dependency on the authors' own work; however, it does not make the paper's claims equivalent to their inputs. The apparent swap of companion and conjoint conditions between Explication 3.17 and the proof of Theorem 3.18 is a correctness issue to be fixed, not a circular reduction. Accordingly, the circularity score is 2: no circular step, but a notable self-referential proof deferral.

Assumptions & free parameters 0 free parameters · 5 assumptions · 2 invented entities

No numeric free parameters are fitted, and no data are involved. The framework rests on newly defined 2-categorical machinery whose proofs are deferred to a companion manuscript, and on prior categorical infrastructure such as adequate triples, ℱ-sketches, spans, and lenses taken as background.

assumptions (5)
  • ad hoc to paper The 2-category of loose bimodules is cartesian and restriction is a pseudo-functor preserving symmetric monoidal and cartesian structure.
    This is the technical foundation of the paper. The proof is deferred to the authors' companion manuscript [BCLJ25], listed as in preparation, in particular Theorems 3.15, 3.18, and 3.23.
  • domain assumption A systems theory is faithfully represented by a symmetric monoidal loose right module.
    This definitional choice is the interpretive core of Section 4. It is assumed rather than derived from any external benchmark.
  • domain assumption The examples satisfy the exactness properties claimed: Petri is rex, Euc is a cartesian differential category, Set and Meas support the relevant endofunctors, and free rex and lex categories classify wiring diagrams.
    These facts are taken from cited literature such as [BM20], [CCGZ24], [FS18c], and [Mye21], and are not proven in this paper.
  • standard math Adequate triples, the span construction, and the lens construction correctly encode the interaction patterns used throughout.
    The paper relies on [HHLN20], [DPP10], [Mye20], and [Spi19] for these background constructions, and uses them as given.
  • ad hoc to paper The labeling definition of loose bimodules is equivalent to the expected notion of pseudo-bimodule.
    Section 3.2 sketches this equivalence and defers the full proof to [BCLJ25], so the paper's foundational identification is not fully established in the preprint.
invented entities (2)
  • Loose bimodule defined as a double functor into the walking loose arrow (double barrels).
    purpose: Technical foundation for modules of systems, intended to describe left and right actions of double categories.
    This is a new formal gadget introduced by the authors. Its complete theory is deferred to the companion manuscript [BCLJ25] and no independent formalization or reproduction is provided here.
  • Symmetric monoidal loose right module interpreted as a module of systems.
    purpose: Packages systems, interfaces, interactions, and maps between them into a single structure.
    This is an interpretive and organizational structure proposed by the paper; its usefulness and coherence are asserted through examples rather than demonstrated by independent evidence.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Towards a double operadic theory of systems." pith.science (2026). https://pith.science/paper/RUJAQIQI

@misc{pith2026250518329,
  author       = {Pith},
  title        = {Pith review of: Towards a double operadic theory of systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RUJAQIQI}},
  note         = {Machine review of arXiv:2505.18329}
}
read the original abstract

We present a unified framework for categorical systems theory which packages a collection of open systems, their interactions, and their maps into a symmetric monoidal loose right module of systems over a symmetric monoidal double category of interfaces and interactions. As examples, we give detailed descriptions of (1) the module of open Petri nets over undirected wiring diagrams and (2) the module of deterministic Moore machines over lenses. We define several pseudo-functorial constructions of modules of systems in the form of doctrines of systems theories. In particular, we introduce doctrines for port-plugging systems, variable sharing systems, and generalized Moore machines, each of which generalizes existing work in categorical systems theory. Finally, we observe how diagrammatic interaction patterns are free processes in particular doctrines.

Figures

Figures reproduced from arXiv: 2505.18329 by the authors.

Figure 1
Figure 1. Ontology of double categorical systems theory [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Systems theory as labelled double category [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Ontology of double categorical systems theory [PITH_FULL_IMAGE:figures/full_fig_p033_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Doctrine of systems theories into the 2-categories of loose right modules and double categories. We often notate such a doctrine by the triple, (𝜋𝒟 : 𝒟sys → 𝒟inter, S, I). A doctrine induces pseudofunctors 𝒮M(𝒟sys) → 𝒮M(ℓℳodr) and 𝒞art(𝒟sys) → 𝒞art(ℓℳodr), and similarl…

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Double-functorial representation of regular hyperdoctrines

    math.CT 2025-08 unverdicted novelty 6.0 of 10

    Regular hyperdoctrines are equivalently described as lax symmetric monoidal pseudo double functors from spans to quintets whose monoidal laxators provide companion commuter cells.

  2. Dynamical Systems as Functorial Realisations of Abstract Evolution Shapes

    math.CT 2026-07 accept novelty 5.0 of 10

    A categorical framework defines dynamical systems as functors from abstract evolution shapes to coefficient categories, with convergence and Lyapunov stability expressed through cosieve filters and sublevel neighbourhoods.

  3. Double Categories of Open Systems: the Cospan Approach

    math.CT 2025-09 conditional novelty 4.0 of 10

    Structured and decorated cospan double categories for open systems have an exoskeleton/outer shell structure, and every object in them is a special symmetric Frobenius pseudomonoid.

Reference graph

Works this paper leans on

2 extracted references · 1 linked inside Pith · cited by 3 Pith papers

  1. [2025]

    The Behavioral Approach to Open and Interconnected Systems

    doi: 10.48550/ARXIV.2502.10368. url: https://arxiv.org/abs/2502.10368. [VSL14] Dmitry Vagner, David I. Spivak, and Eugene Lerman.Algebras of Open Dynamical Systems on the Operad of Wiring Diagrams. 2014. doi: 10 . 48550 / ARXIV . 1408 . 1598. url: https : //arxiv.org/abs/1408.1598. [Wei09] Alan Weinstein.Symplectic Categories. 2009.doi: 10.48550/ARXIV.091...

    arXiv doi:10.48550/arxiv.2502.10368 2014

  2. [2962]

    Cartesian double theories: A double-categorical framework for categorical doctrines

    doi: 10.1098/rsta.2021.0309. url: http://dx.doi.org/10.1098/rsta.2021.0309. [Lor25] Fosco Loregian.Monads and limits in bicategories of circuits. 2025.doi: 10.48550/ARXIV.2501. 01882. url: https://arxiv.org/abs/2501.01882. [LP24] Michael Lambert and Evan Patterson. “Cartesian double theories: A double-categorical framework for categorical doctrines”. In:A...

    arXiv 2021

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.