Bayes as lenses

Jules Hedges mentioned on Twitter that Bayesian updates could be described as two morphisms \(\mathbf{C}(S, DA)\) and \(\mathbf{C}(DS \times B, DT)\), but it was “too much squinting” to make them a lens.

I have not been able to follow if there was any update on that, but in case this is still useful to anyone, let us get Bayes update as an optic.

\begin{aligned} & \int^{C \in \mathbf{EM}} \mathbf{EM}(DS , C \times DA) \times \mathbf{Kl}(C \rtimes B, T) \\ \cong & \\ & \mathbf{C}(S, DA) \times \mathbf{C}(DS \times B , DT). \end{aligned}

Here \(C\) ranges over the Eilenberg-Moore category, but then we forget its algebra structure so it can act on the Kleisli category.