[lcc-0011]

Let B: \mathcal {C}^\mathrm {op} \to \mathsf {Cat} be an indexed category. Recall in the vein of Categorical Systems Theory the categories of charts, given as the Grothendieck construction \int B, and the category of lenses which is the fiberwise opposite \int B(-)^\mathrm {op}.

Suppose \mathcal {C} has pullbacks, each B(X) has pullbacks, and these are preserved by each B(f) =: f^*. Then also the Grothendieck construction \int B has pullbacks. Then we can form \mathsf {\mathbb Span}(\int B).

In this situation, we have an obvious identity-on-objects embedding of the charts \int B \hookrightarrow \mathsf {\mathbb Span}(\int B), and a not-so-obvious embedding of the lenses \int B^\mathrm {op} \hookrightarrow \mathsf {\mathbb Span}(\int B), given by carrying a lens \binom {f^\#: f^*B \to A}{f: X \to X'}: \binom {A}{X} \leftrightarrows \binom {B}{Y } to the span whose apex is \binom {f^*B}{X}, whose backwards leg is \binom {f^\#}{1_X}, and whose forwards leg is \binom {\bar {f}}{f}. where \bar {f} is the unique Cartesian lift of f to f^*B \to B

As usual, we can form a double category of spans and morphisms (ie charts), which would receive a functor from the usual double category of lenses and charts. However, in this case, it may in fact be just as useful to take the double category of spans and lenses, since, if we use these to compare systems with the objects of \int B as interfaces, we get a profunctor associated with a span - and this is the role usually played by charts in categorical systems theory

It's worth noting that the assumptions about pullbacks are fairly strong - for example, the category of (smooth) manifolds does not have pullbacks.

Now suppose T: \mathcal {C} \to \int B is a tangent bundle functor in the sense of Myers, let X, X' \in \int B be interfaces, and let S,S' be state spaces. A span X \nrightarrow X' is suitable for thinking about bisimulation - for example, a 2-cell filling this square:

is a witness that those two span form a bisimulation between the open systems

However, by including lenses as well as charts, these spans(or the relations they present) can describe some additional situations. For example, in Robust control for dynamical systems with non-gaussian noise via formal abstractions, we consider a partition of a state space \mathbb {R}^n into a discrete set of convex pieces. This is essentially a lens (see https://erischel.com/lcc-0010/ for more on this), but there is the small issue of how to define the forwards direction on the boundaries between the pieces. We can sidestep this by noting that we can easily define a span of charts as discussed here. This span is seen to have the property that any controller for the codomain (i.e a lens Y \to I) lifts to one for the domain which is related by bisimulation.