Remark [efr-I1K5]

The preceding definition clearly works in a non-symmetric monoidal category as well. In this case, arguably, a context should be defined to consist of maps I \to M_1 \otimes X \otimes M_2, M_1 \otimes Y \otimes M_2 \to I. However, the problem with this from our point of view is that it doesn't allow the definition of a costate on P given a parametrized map (since one cannot commute the P past the M_1), which is what we're interested in.

It is also worth observing that contexts are essentially the same thing as optics {I \choose I} \to {Y \choose X}. We have not specified an equivalence relation on contexts (we do not need it,) but it is easy to see that for any parametrized map, two contexts that are sliding equivalent give the same induced costate.