Proposition [efr-0029]

Given a lens A \leftrightarrows A', postcomposition gives a functor \mathsf {Sys}(A) \to \mathsf {Sys}(A'). Given a chart A \rightrightarrows A', there is a profunctor \mathsf {Sys}(A) \nrightarrow \mathsf {Sys}(A'), where the set over TS \leftrightarrows A and TS' \leftrightarrows A' is the set of maps S \to S' so that this square commutes:

This defines a double functor \mathsf {Sys}: \mathsf {\mathbb Arena} \to \mathsf {\mathbb Cat}.