Definition Internally iterable [efr-87W1]

Let \mathcal {C} be a Markov category, let A be an object, and let m be a midpoint algebra on A, i.e a midpoint algebra structure on each \mathcal {C}(X,A), natural in X. Then A is internally iterable if, for each X \to X \otimes A \in \mathcal {C}, there exists a unique map u: X \to A satisfying u = m(u \pi _X, \pi _A)s