Let m_1,m_2 denote two coinflip structures. Let \mu _1 = m_1(\pi _1, \pi _2) : A \otimes A \to A, analogously \mu _2 (we condense the notation by writing \mu _1,\mu _2 regardless of the object in question). Note m_1(a,b) = \mu _1\langle a,b \rangle , where \langle a,b \rangle is any pairing of a,b, by naturality.

First consider m_1(m_2(a,b),m_2(c,d)). By the above this is \mu _1 \langle \mu _2 \langle a,b \rangle , \mu _2 \langle c,d \rangle \rangle . Applying naturality to the morphism \mu _2, we can also rewrite this as \mu _2 \circ (m_1(\langle a,c \rangle ,\langle b,d \rangle ))

Now take c = b, d = a. By symmetry for m_2 we can rewrite the left-hand side as m_1(m_2(a,b),m_2(a,b)). By idempotency this is simply m_2(a,b). The other expression now becomes \mu _2 \circ (m_1(\langle a,b \rangle ,\langle b,a \rangle )). Now consider the first projection of the map m_1(\langle a,b \rangle ,\langle b,a \rangle ). By naturality it is equal to m_1(a,b). By symmetry, so is the second projection. Hence this is a pairing of m_1(a,b) with itself. Hence the composite is equal to m_2(m_1(a,b),m_1(a,b)) = m_1(a,b). This concludes the proof.

Let f be a coinflip. Consider the map 2 \xrightarrow {\oplus f} 2 given by flipping the coin, applying \neg : 2 \to 2 in one branch and doing nothing in the other. We claim this is equal to deletion followed by the coinflip. This can be checked on each summand (since 2 is a coproduct), where it follows by symmetry.

Now let f_1, f_2 be two coinflips and consider the operation given by 1 \xrightarrow {f_1 \otimes f_2} 2 \otimes 2 \xrightarrow {\oplus }. This is easily seen to be equal both to f_1 ; (\oplus f_2) and f_2 ; (\oplus f_1). But these are equal to f_2 and f_1 respectively by the above.

Let A be an iterable midpoint algebra. Note that any map f: [0,1] \to A must be a homomorphism for the infinitary midpoint operator M. Hence given a_0,a_1 \in A, the unique f so that f(0) = a_0, f(1) = a_1 is given by f(0.b_1b_2 \dots ) = M(a_{b_1}, \dots ). This is straightforwardly seen to be well-defined and a midpoint homomorphism.

We identify the elements of \bar {\Delta }(X) with countably supported probability measures on X. Observe that \bar {\Delta } X is an iterable midpoint algebra (with the infinitary choice operation given by the sum M((a_i)) = \sum _i 1/2^i a_i). By the preceding, every finitely supported measure can be obtained by iterating M, and every countably supported measure can be obtained by applying M to a sequence of these (half of the probability measure must be concentrated in some finite subset, then 1/4 of the remainder again in some finite subset, and so on). Hence there is at most one midpoint homomorphism \bar {\Delta }X \to Y extending any given function f: X \to Y, for any iterable midpoint algebra Y.

Now we must show that one exists. By a finitary dyadic measure, we mean one which is finitely supported and where each weight a_x has the form k/2^n. Note that these are exactly those that can be written using just the binary choice operator m(x,y). Also note that any two such terms are equal in a generic midpoint algebra if and only if they represent the same such measure. Hence given f: X \to Y, there is a unique and well-defined f(a) defined on the finitary dyadic measures, which is a midpoint homomorphism.

Now for any probability measure \mu , we can write it as \mu = M(a_1,\dots ), where each a_i is a finitary dyadic measure. We define our operation as f(\mu ) = M(f(a_1), \dots ), with f(a_i) defined as above. It suffices to show that this is well-defined, since f(m(\mu ^1,\mu ^2)) = f(m(M(a_1^1,\dots ),M(a_1^2,\dots ))) = f(M(m(a^1_1,a^2_1), \dots )) = M(m(f(a_1^1),f(a_1^2)),\dots ) = m(f(\mu ^1),f(\mu ^2))

Now let M(a_1,\dots ) = M(b_1,\dots ) = \mu be two representations in this form of the same measure. Then there exists some smallest N so that there exists a finitary dyadic probability measure c_1 = \sum _i \frac {k_i}{2^N} \delta _{x_i} so that k_i/2^N < 2 \mu (x_i) whenever this is positive - that is, so that c/2 is strictly less than \mu everywhere on the support.

Now in the sum \sum _i 1/2^i a_i must exceed c/2 by some finite partial sum, say M. Then \sum ^M_{i=1} 1/2^i a_i is a finitary dyadic measure. Hence a finite manipulation using the properties of midpoint algebras can rewrite the term M(a_1,\dots ) into M(c_1,a_2',\dots ,a_M',a_{M+1}). Iterating this we build c_2,\dots so that M(a_1,\dots ) = M(c_1,\dots ). Since these only depended on the measure \mu , we similarly find M(b_1,\dots ) = M(c_1,\dots ). Since this argument used only the axioms of an iterable midpoint algebra, it follows that f is well-defined.

Let s: X \to A \otimes X be a map, and suppose u_1,u_2 both satisfy the equation u_i = m(\pi _A s, u_i \pi _X s). Let a_n : X \to A denote the map defined inductively by a_1 = \pi _A s, a_{n+1} = a_n \pi _X s. Let b_i^{n} be defined inductively by b_i^1 = u_i, b_i^{n+1} = b_i^n \pi _X s. Then we see that b_i^n = m(a_n, b_i^{n+1}) for both i=1,2. Therefore they must agree, and in particular u_1 = u_2. This concludes the proof.

By Reference [escardo-simpson-universal-interval-2001], a midpoint algebra (A,m) in \mathsf {Set} is iterable if and only if is satisfies these conditions:

1. There exists an operator M: A^\omega \to A so that M(a_1,a_2, \dots ) = m(a_1, M(a_2, a_3, \dots ))
2. Given two sequences a_i, b_i so that b_i = m(a_i, b_{i+1}) for all i, then b_1 = M(a_1, a_2, \dots )

Let a countable family f_i : A \to B be given. Consider the operation \sum ^\omega _{i=0} A \to B \times \sum ^\omega A given by the copairing of all the f_i paired with the map \sum ^\omega _{i=0} A \to \sum ^\omega _{i=0} A which maps each summand to the next one (i.e (i,a) \mapsto (i+1,a)). Now an iteration of this map u: \sum _i A \to B is equivalently a sequence of maps g_i so that g_i = m(f_i,g_{i+1}). Hence the existence and uniqueness of such an operator precisely corresponds to points 1 and 2 above.