Definition [efr-001C]
Definition [efr-001C]
Let \Delta : \mathsf {Set} \to \mathsf {Set} carry a set X to the set of finite-support probability distributions on X. Recall that \Delta is a monad.
Given two indexed sets \bar {X} \to X, \bar {Y} \to Y, an indexed stochastic lens \binom {\bar {X}}{X} \to \binom {\bar {Y}}{Y} is an element of the convex space \prod _{x \in X} \sum _{y \in Y} [\Delta (\bar {Y}_y),\Delta (\bar {X}_x)], where the internal hom, product and coproduct are taken in the category of convex spaces. Note that if each \bar {Y}_y is identical, say B, this is isomorphism to \prod _{x \in X} \Delta (Y) \otimes [\Delta (B),\Delta (\bar {X}_x)]. Recall also that an element of [\Delta (X),\Delta (Y)] is equivalently a function X \to \Delta (Y), i.e. a Kleisli map X \to Y.
An indexed stochastic chart is an element of the convex space \prod _{x \in X} \sum _{y \in Y} [\Delta (\bar {X}_x),\Delta (\bar {Y}_y)]