Definition \mathsf {\mathbb Ctrl} [efr-000I]

Let \mathcal {C}, \mathcal {A}(-), T be a dynamical systems theory, let \mathsf {\mathbb Arena} be the associated category of arenas. Recall that \mathsf {\mathbb Arena}_0 is the category of lenses. Consider the (strict) category internal to \mathsf {Arr}(\mathsf {SymMonCat}) given by the following diagram:

By Theorem [efr-003R], the image of this internal category under \mathsf {\mathbb Para}(-) is a iwss triple category. We call this triple category the triple category of controlled processes, and denote it by \mathsf {\mathbb Ctrl}, or \mathsf {\mathbb Ctrl}_{T,\mathcal {C},\mathcal {A}} if we want to disambiguate the choice of doctrine.

(Note the difference between \mathsf {Arr}(\mathcal {C})^\simeq and \mathsf {Arr}(\mathcal {C}^\simeq )---the former has objects all morphisms of \mathcal {C}, and the morphisms between them given by isomorphisms, whereas the latter has objects only the isomorphisms in \mathcal {C})