Iterability for probability (pro)monads [efr-557J]

Let P be an affine symmetric monoidal (pro)monad (i.e Markov Promonad). Suppose the underlying \mathcal {C} is distributive, it preserves finite coproducts (eg if it's a monad), and there is a coinflip, so that each homset acquires the structure of a midpoint algebra. If P additionally has Kolmogorov products, under mild assumptions on \mathcal {C} we additionally get a countable-arity operation P(X)^n \to P(X) (or the equivalent for promonads) which corresponds to the linear combination M(\mu _1, \dots ) = \sum _{i=1} \mu _i /2^i of distributions. This satisfies M(\mu _1, \dots ) = m(\mu _1, M(\mu _2, \dots )) for obvious reasons.

If this equation characterizes it uniquely (in a pointwise sense), Escardo-Simpson would call this midpoint algebra iterable. We can add this as an axiom to our probability promonad.

This essentially says, if I have a sequence \mu _i of distributions, then there is a unique sequence \nu _i so that \nu _i = m(\mu _i, \nu _{i+1}). In other words given two such sequences, they agree, and in particular their first elements agree.

We can also weaken this in a way which is equivalent given countable choice: Suppose \nu ,\nu ' are such that for all N \in \mathbb {N}, there exists \nu = \nu _1, \nu _2, \dots \nu _N, \nu ' = \nu '_1, \nu '_2, \dots \nu '_N so that \nu _i = m(\mu _i, \nu _{i+1}) and the same for \nu ' (but only for i < N). We can assert given this, \nu = \nu '. This says "assuming for all n, they are within 1/2^n of each other, then they are equal.

It seems that the latter is enough to prove that every Dedekind real corresponds to a (decidable) probability.

We might call this latter condition strong iterability, although note that this should certainly come with some other conditions (like the Kolmogorov axiom) ensuring that we can actually iterate probabilities.