Given an indexed category \mathcal {A}: \mathcal {C}^\mathrm {op} \to \mathsf {Cat}, the double category \mathsf {\mathbb Arena} of arenas has
Objects the objects of \int \mathcal {A}---note that these are the same as the objects of \int \mathcal {A}(-)^\mathrm {op}
Vertical morphisms the lenses
Horizontal morphisms the charts
The double category is thin. Given a square of this form
we can first project it to a square in \mathcal {C}. If this commutes, we can pull the lenses and charts back to a square in \mathcal {A}(A_1). The above square of lenses and charts will be said to commute if both of these squares commute.
