Proof Proof of Theorem [efr-FTTL] [efr-T2PU]

Let \mathcal {C} be a \kappa -distributive externally iterable coinflip Markov category. There is an essentially unique \kappa -coproduct preserving Markov functor F: \mathsf {Set}^{< \kappa } \to \mathcal {C} (since \mathcal {C}_\mathrm {det} is \kappa -distributive and \mathsf {Set}^{< \kappa } is initial such). Any extension to the stochastic morphisms is determined by its action on the homsets \mathsf {Set}_{\bar {\Delta }}^{< \kappa }(*,X) = \bar {\Delta }(X), by the coproduct universal property. On these its action must be given by taking a convex combination \sum _i \epsilon _i x_i to the convex combination \sum _i \epsilon _i F(x_i). This is functorial by Corollary [efr-REOY], finishing the proof.