Some Notions of (Open) Dynamical System on Polynomial Interfaces

The paper proves that in discrete time T = N, Dyn_N(p) is equivalent to p-Coalg by (i) identifying objects via p/S ≅ ∑_{i:p(1)} S^{p[i]} and the universal property of dependent sums, and (ii) showing the coalgebra-homomorphism equation β′ ∘ f = (p/f) ∘ β is equivalent to the Dyn_N(p) naturality squares for every section σ, using pullbacks and a sequence of bijective rewrites. This is Proposition 3.44, with the discrete-time reduction in Proposition 3.19 and the morphism condition from Proposition 3.15, all set in a locally cartesian closed category E (Definition 1.1). The candidate solution reproduces exactly this construction: it spells out the p/X computation, the object-level bijection (output map and dependent update), the discrete-time flow via iteration, and the morphism equivalence—then explicitly packages these into inverse functors F and G that are inverse on the nose. The arguments line up step-for-step with the paper’s proof and fill in the same universal-property transpositions; no essential hypotheses are missing beyond those the paper already assumes (E LCCC, discrete time N). Therefore, both are correct and essentially the same proof. Key places in the paper: the LCCC setup (Definition 1.1), the discrete-time reduction (Proposition 3.19), the main equivalence (Proposition 3.44, including object/hom-set bijections), and the Dyn_N(p) morphism squares used in the hom-set correspondence.