\mathsf {BiSys}(\mathcal {C},\mathcal {A},T) has the following structure: The objects are simply the objects of \mathcal {A}---the bundles.
There are three types of 1-cell: Lenses, that is morphism in \mathcal {A}^\mathrm {fop}, which we write A \leftrightarrows B, charts, that is morphisms in \mathcal {A}, which we write A \rightrightarrows B, and bisystems, which are pairs (S \in \mathcal {C}, TS \otimes A \leftrightarrows B), and which we write A \nrightarrow B.
Moreover there are three types of 2-cell:
Lens-chart cells, which are the 2-cells of \mathsf {\mathbb Arena}(\mathcal {A}). Note that this double category is thin. We will say a square of lenses and charts commutes if it is filled by such a 2-cell.
Chart-bisystem cells---given charts A_1 \rightrightarrows B_1, A_2 \rightrightarrows B_2 and systems TS \otimes A_1 \leftrightarrows A_2, TS' \otimes A_2 \leftrightarrows B_2, a square filling this is a choice of map S \to S' \in \mathcal {C} so that the resulting lens-chart square
commutes.
Lens-bisystem cells. Given lenses A_1 \leftrightarrows B_1, A_2 \leftrightarrows B_2, and systems TS' \otimes A_1 \leftrightarrows A_2, TS' \otimes B_1 \leftrightarrows B_2, a 2-cell consists of an isomorphism S' \xrightarrow {\sim } S' so that the resulting square of lenses commutes (recall that isomorphism charts are the same as isomorphism lenses).
The charts, bisystems and chart-bisystem cells form a pseudo double category with the obvious composition. So do the lenses, bisystems and lens-bisystem cells. Finally, there is a notion of 3-cell given by a box whose sides are 2-cells of each kind, so that the resulting diagram in \mathcal {C} (with isomorphisms on two sides) commutes.
The lens-bisystem double category is \mathsf {\mathbb Para}_{\mathcal {C}^\simeq }(\mathsf {\mathbb Arena}{\mathcal {A}}_0) (recall that \mathsf {\mathbb Arena}{\mathcal {A}}_0 = \mathcal {A}^\mathrm {fop}), with the action given by the functor T (restricted to isomorphisms). The chart-bisystem double category is the result of taking \mathsf {BiSys}(\mathcal {C},\mathcal {A},T), a pseudocategory in double categories, and applying \mathsf {PsCat}((-)_h) : \mathsf {PsCat}(\mathsf {DblCat}) \to \mathsf {PsCat}(\mathsf {Cat}) where (-)_h takes the horizontal category of a (strict) double category.
The 3-cells, of course, are the 2-cells of \mathsf {\mathbb Para}_{(\mathcal {C}^\to )^\simeq }(\mathsf {\mathbb Arena}(\mathcal {A})_1). Analogously to the above, for each class of 1-cells, there is a
double category with those as the objects, the two types of cell as the two morphisms, and the 3-cells as the 2-cells.
All of these six double categories admit a symmetric monoidal structure.
