Definition Behavioural equivalence [efr-X2S5]

Let \mathcal {D} be a monoidal stochastic module. Two precharts f_1, f_2: \bar {X} \to \bar {Y} with the same underlying map X \to Y are said to be behaviourally equivalent if, for any other three charts h: \bar {A} \to \bar {B}, s: \bar {S} \to \bar {A} \otimes \bar {X}, t: \bar {B} \otimes \bar {Y} \to \bar {T} so that the composite map S \to T is deterministic, the composite charts t(h \otimes f_1)s = t(h \otimes f_2)s agree as charts.