I was trying to construct a category of measurable spaces and 'nondeterministic functions' (not the usual category of measurable spaces); specifically a map $(\Omega, \Sigma)\rightarrow (\Omega', \Sigma')$ is a function $f$ from $\Omega$ to the set of all probability measures on $\Sigma'$ such that for each $\sigma'$, the function $\omega \mapsto f_\omega(\sigma')$ is measurable. The idea is that $f(\omega)$ is in $\sigma'$ with probability $f_\omega(\sigma')$. So after defining composition: $$ (gf)_\omega(\sigma'') = \int_{\Omega'} g_{\omega'}(\sigma'')df_\omega(\omega') $$ (here the notation $\int f(x) d\mu(x)$ indicates that $\mu$ is the measure and $x$ the dummy variable), the condition that composition is associative is equivalent to $$ \int_{\Omega'} \left(\int_{\Omega''}h_{\omega''}(\sigma''') dg_{\omega'}(\omega'') \right) df_\omega(\omega')= \int_{\Omega''}h_{\omega''}(\sigma''') d(gf)_\omega(\omega'')$$ Here $f : (\Omega, \Sigma) \rightarrow (\Omega', \Sigma')$, $g : (\Omega', \Sigma') \rightarrow (\Omega'', \Sigma'')$, $h : (\Omega'', \Sigma'') \rightarrow (\Omega''', \Sigma''')$, $\sigma'''\in\Sigma'''$, $\omega \in \Omega$, and the other omegas are dummy variables. Is this known in the literature? I'm not very familiar with measure theory. I strongly suspect that it is true, because all of the other axioms have worked so far (e.g. the composition of two measures really is a measure, identities work out properly). This will probably have a longish, boringish proof involving approximation by simple functions, which I want to avoid going through if someone else has. Indeed, if someone else has proven this, perhaps the category I am considering has already been invented. Does it look familiar to anyone? Perhaps a version of the chain rule, but for integrals?
Edit: The proof of this is actually shorter than I had thought. However, the maps have already been studied; see the answer(s).
