Definition \mathsf {BiSys} [efr-EPI9]

Let \mathcal {A} \to \mathcal {C}, T: \mathcal {C} \to \mathcal {A} be a symmetric monoidal dynamical systems theory. Then this diagram:

depicts two strict double categories, each with a symmetric monoidal structure, and a strict double functor between them which is (non-strictly) a symmetric monoidal functor. This induces an object of \mathsf {SymMon}(\mathsf {Act}(\mathsf {DblCat})). Applying \mathsf {\mathbb Para}(-) under \mathsf {SymMon}(-), we obtain a symmetric pseudomonoid in internal pseudocategories in \mathsf {DblCat}. Denote by \mathsf {BiSys}(\mathcal {C},\mathcal {A},T) this induced object.