Proposition [efr-000J]
Proposition [efr-000J]
The objects of \mathsf {\mathbb Ctrl} are arenas.
The three directions of morphism in \mathsf {\mathbb Ctrl} are lenses, charts, and controlled processes.
The lens-chart double category is isomorphically \mathsf {\mathbb Arena}---in particular, composition of both lenses and charts is strictly associative.
The process-chart double category has 2-cells the chart reparametrizations. The process-lens double category has 2-cells the lens isoparametrizations. They both compose in the obvious way.
Processes compose as morphisms of \mathsf {Para}_{\mathcal {C}^\simeq }(\mathsf {Lens})---that is, (S,TS \otimes A \to B) ; (S', TS' \otimes B \to C) = (S' \otimes S, T(S' \otimes S) \otimes A \cong TS' \otimes TS \otimes A \to TS' \otimes B \to C), this is associative up to a coherent choice of globular isoparametrization.