Definition Controlled Lens [efr-000B]

Let (\mathcal {C},\mathcal {A},T) be a monoidal theory of dynamical systems. Then the double category of controlled lenses is defined as follows:

1. The objects are the arenas, objects of \int \mathcal {A}
2. The vertical category is simply the category of charts
3. A horizontal morphism is a controlled lens, a tuple S \in \mathcal {C}, TS \otimes A \to B
4. Horizontal composition is by tensoring
5. A 2-cell is a map S \to S' so that the induced diagram in the double category of lenses and charts commutes.

We could extend this to a triple category, where the third type of morphism is a bare lens, and a commutative square of controlled lenses and bare lenses must satisfy a different commutativity equation.