{'fraction_non_alphanumeric': 0.036280765724703734, 'fraction_numerical': 0.00846464383383253, 'mean_word_length': 4.316532816394351, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 16, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
De Finetti's Theorem in Categorical Probability

We present a novel proof of de Finetti's Theorem characterizing permutation-invariant probability measures of infinite sequences of variables, so-called exchangeable measures. The proof is phrased in the language of Markov categories, which provide an abstract categorical framework for probability and information flow. The diagrammatic and abstract nature of the arguments makes the proof intuitive and easy to follow. We also show how the usual measure-theoretic version of de Finetti's Theorem for standard Borel spaces is an instance of this result.


Introduction
De Finetti's Theorem states that every permutation-invariant joint probability distribution of countably many random variables is such that these variables are conditionally independent given a suitable latent variable. Moreover, a canonical choice of the latent variable is the empirical distribution of the variables under consideration (which exists almost surely). In this paper, we state and prove a more abstract version of de Finetti's Theorem in the context of categorical probability theory, which is a nascent framework for a foundation of probability and statistics that is more abstract and more general than the traditional measure-theoretic approach.
Context of de Finetti's Theorem. To provide some context for and illustrate the significance of de Finetti's Theorem, it is helpful to consider the notoriously divisive debate on the subjective vs. objective view on probability [22,32]. For our purposes, note that there are situations in which it is commonly presumed that one can give objective meaning to probability and infer its value. For example, flipping a coin and counting the relative frequency of 'heads' among the trials ought to converge to the bias of the coin. This is the content of the law of large numbers.
However, there is no free lunch and the assumption that the objective probability exists is crucial in the above reasoning. As de Finetti eloquently argues in Section 3 of [11], from the subjectivist point of view, "nothing obliges us to choose [probability of heads in the next toss] to be close to the frequency [of heads in the previously observed tosses]." Let us give a brief account of the argument here and refer to de Finetti's classic [11] for more details.
In the coin-flipping experiment, suppose that we are given a (subjective) joint probability distribution over possible sequences of heads and tails. If the coin had an associated bias that does not change from one trial to the next, we would expect the outcomes of different trials to be conditionally independent, given the knowledge of the bias. In such case, however, the bias is an (objective) property of the coin that corresponds to the probabilities that the coin lands heads or tails respectively. On the flip side, it is unclear how to justify trial independence without implicitly bringing in the assumption of objective probability. Nevertheless, we may require that the joint distribution is unchanged under permutations of the different trials, a property known as exchangeability 1 which expresses the belief that these are trials of the "same phenomenon".
De Finetti shows that with respect to any exchangeable probability measure, the individual trials are conditionally independent given some random variable Y . Moreover, there is a canonical choice for Y whose values precisely correspond to the possible biases of the coin, so that (in this example) Y takes values in the unit interval [0, 1]. De Finetti's Theorem thus justifies the use of probability distributions in the subjectivist conception, since it says that exchangeable behaviors (of infinitely many trials) are indistinguishable from the behaviors of a repeated flipping of a coin with unknown, but fixed, bias.
Indeed, one can easily see that flipping a coin with an unknown bias, distributed according to some probability measure on Y , leads to a distribution of sequences of heads and tails that is exchangeable. The non-trivial part of de Finetti's Theorem is in the converse. It says that, given a countable number of trials, every exchangeable distribution arises in this way.
Historically speaking, the above context is the one in which the topic of our paper de Finetti's Theorem originates. However, besides its implications for the foundations of the concept of probability, the result also bears significance for the development of nonparametric Bayesian modelling [24,31]. More concretely, many natural stochastic processes such as drawing with replacement (e.g. the Pólya urn model and modifications thereof) or without replacement give rise to exchangeable distributions. By de Finetti's Theorem, they can be equivalently described as drawing a random probability distribution q according to a specified prior distribution over distributions, µ (e.g. a Dirichlet process), and subsequently drawing independent samples from q. In other words, they correspond to a mixture of iid (independent and identically distributed) samplings, which is useful both as an aid for intuitive understanding and for concrete calculations.
Existing proofs and variants of de Finetti's Theorem. The original proofs by de Finetti in the binary case (as in coin-flipping) can be found in [10,11], while a more general result is due to Hewitt and Savage [21], who have shown the analogous statement for exchangeable Radon probability measures on compact Hausdorff spaces. We give more details on the measure-theoretic formulation for standard Borel spaces in Section 2. Since then, many proofs based on different methods have appeared in various contexts. For instance, those of [26,Theorem 11.10] and [4, Theorem 3.1] use the mean ergodic theorem and conditional expectations; in [29,Theorem 12.17] and [3,Theorem 3.1] one arrives at the result via backwards martingales; while harmonic [30] and non-standard [2] analysis have also been used. The latter has recently led to a new generalization of de Finetti's Theorem for exchangeable Radon measures on any Hausdorff space [1]. Functional analysis and moment methods have been utilized in the proof from [15, Chapter VII], whose more elementary and explicitly calculational version that applies to binary variables can be found in [28].
Very recently, Jacobs and Staton [23] have presented a category-theoretic approach to de Finetti's Theorem, different from the present one, for the binary case. Therein, the statement of de Finetti's Theorem is encoded in the fact that the unit interval the space of probability distributions arises as the categorical limit of a sequence of multisets over {0, 1} ("urns") related by morphisms that represent the action of drawing a random element from an urn without replacement.
Our version of de Finetti's Theorem. In Section 4, we present an abstract version of de Finetti's Theorem as a statement about morphisms in categories which admit notions of parallel composition, swapping, copying, and discarding, called Markov categories [17]. The framework of Markov categories is very general, and there are many Markov categories in which de Finetti's Theorem does not hold. Correspondingly, there are additional axioms that enter as ingredients in the proof of our abstract version of de Finetti's Theorem. Specifically, they correspond to the fact that one should be able to • construct conditional probabilities, • describe distributions on spaces of probability distributions, and • consider countable sequences of trials. These three requirements will be stated formally in Assumption 4.2, after introducing the basics of the formalism of Markov categories in Section 3. Within a Markov category that satisfies them, one therefore obtains a version of de Finetti's Theorem. As we show in Section 4, the measure-theoretic version for discrete and continuous random variables (described by standard Borel spaces) arises in this way as well. Additionally, we automatically get a characterization of exchangeable Markov kernels, unlike the classical results that focus exclusively on exchangeable measures. As far as we know, this result has not appeared in the literature before.
It is likely that other Markov categories also have the required properties, and that instantiating the abstract de Finetti's Theorem in those leads to a context in which the result would be entirely new. However, we do not know of any such examples at present and leave the search for these to future investigations.
Synthetic probability theory. The process described above identifying abstract results that follow from properties expressed within the framework and instantiating them in concrete Markov categories is an example of the synthetic approach to probability theory, which is distinguished from the standard analytic one in terms of measure theory by encapsulating measure-theoretic statements in suitable higher-level axioms [17]. It differs from standard approaches by using more formal and abstract reasoning and it only depends on the particular measuretheoretic semantics insofar as the synthetic axioms may or may not be satisfied. A number of concepts and theorems of classical probability and statistics have been given a synthetic treatment in recent years [7,17,19,18]. We recall the ones relevant for de Finetti's Theorem in Section 3.
The proof that we present in Section 5 is inspired by several of the concrete ones mentioned above, but as far as we know it does not match either of them completely. Its abstract nature, which places the focus on essential aspects while allowing us to ignore irrelevant details, arguably makes it easier to follow than any measure-theoretic one, although it is still far from obvious. The proof relies on the graphical calculus of string diagrams, which captures several non-trivial properties implicitly and whose connectivity explicitly depicts information flow. It is these two features that enable one to readily interpret any stage of the proof with relative ease, once some familiarity with the diagrammatic notation has been obtained.
Outlook. Given the intuitive nature of our proof, it is natural to hope that even deeper results can be proven along similar lines in a purely synthetic manner, and that one can ultimately aim at proving new statements that would be too difficult to obtain in the traditional measure-theoretic formalism due to its higher complexity. With this in mind, it may be worth mentioning a few extensions of de Finetti's Theorem which one can try to aim at next.
Among the most interesting variations on the exchangeability theme is arguably the notion of partial exchangeability [14], where the invariance under finite permutation invariance is relaxed to invariance under certain structure-preserving permutations. For example, the Aldous-Hoover Theorem [3,4] characterizes exchangeable arrays of random variables and is closely related to random graphs. There is a similar result for Markov chains [12, 13,6]. More recently, partial exchangeability has been generalized to hierarchical exchangeability [5,25]. The work of Crane and Towsner provides perhaps the most general currently available results along these lines [8,9], situated in a model-theoretic framework.

Measure-Theoretic Version of de Finetti's Theorem
Let us turn to a more formal exposition of de Finetti's Theorem in standard measure-theoretic language. Given a measurable space X, consider the product X N of countably many copies of X, equipped with the product σ-algebra. A bijection N → N which fixes all elements apart from a finite subset is called a finite permutation. Given a finite permutation σ : N → N, we denote by n σ ∈ N the largest natural number not fixed by σ.
Consider a probability measure p on X N . By convention, given a finite collection of measurable subsets S 1 , . . . , S n ⊆ X, we write as shorthand for the probability of the "cylinder" event These probabilities specify the marginal distribution of p on the first n components of X N . We say that the measure p is exchangeable if for every finite permutation σ and for every finite sequence of measurable subsets S 1 , . . . , S nσ ⊆ X, we have As we saw in the introduction, a somewhat trivial example of exchangeable measures is given by product measures, i.e., ones satisfying Such a product measure q constitutes the law of a sequence of iid random variables.
Having introduced the notion of exchangeability, we now turn to de Finetti's Theorem itself. A convenient way to express the statement, which lends itself well to category-theoretical translations, is to use the concept of measures on a space of measures, as done by Hewitt and Savage [21, Section 2] among others. If X is a standard Borel space, we denote by P X the set of probability measures on X. The set P X can be equipped with a canonical σ-algebra, namely the one generated by the functions ε f : P X → R given by for all bounded measurable functions f : X → R. Measures on P X (thus elements of P P X) can be thought of as random measures on X, where also the specific form of the distribution is subject to uncertainty. 2 Equivalently, measures on P X describe mixtures of measures either in the sense of finite convex combinations or integrals. Indeed, de Finetti's Theorem can be summarized as the fact that exchangeable measures are mixtures of product measures. Here is the precise statement, in the version for standard Borel spaces.
Theorem 2.1 (de Finetti's Theorem). Let X be a standard Borel space. A probability measure p on X N is exchangeable if and only if there exists a probability measure µ on P X such that for every finite collection of measurable subsets S 1 , . . . , S n ⊆ X, we have For example, the iid case amounts to µ being a delta measure δ r ∈ P P X for some r ∈ P X satisfying p = r N . On the other hand, if µ is a random measure supported on the set {δ x } x∈X of delta measures δ x ∈ P X, then we obtain p 2 Such recursive ways of forming spaces can often be accurately captured by the categorical notion of a monad, and indeed these spaces of measures can be described in terms of a well-known monad, the Giry monad [20]. supported on the diagonal i.e., the set of constant sequences in X N . In other words, the associated exchangeable random variables are then perfectly correlated.
By convex analysis arguments, it can also be shown that given p as in Theorem 2.1, the measure µ is uniquely determined. Note that the result due to Hewitt and Savage [21] is more general than the one above, as it applies to Radon probability measures on arbitrary compact Hausdorff spaces. It includes the uniqueness of µ as well.

Markov Categories
We now take a detour from the discussion of de Finetti's Theorem into the realm of Markov categories. All of the concepts defined in this section have been introduced in earlier works on categorical probability [7,17,19,18]. Nevertheless, in the interest of a self-contained presentation, we recall the main points here in a slightly less formal way, referring to the existing literature for full technical detail.
As mentioned in the introduction, a Markov category is a category that comes with notions of parallel composition, swapping, copying, and discarding. The idea is that contexts in which one wants to model flow of information will generally satisfy these basic requirements and thus correspond to a Markov category. In particular, one would expect that any formalisation of classical probability theory does. However, there are also many Markov categories that have nothing to do with probability theory (see [17]).
One of the simplest interesting examples to keep in mind is FinStoch, the category of finite sets and stochastic matrices. An object in FinStoch is a finite set, which can be interpreted as the set of possible values of a random variable. A morphism, say f : A → X, assigns a probability measure on the finite set X to each element of the finite set A. It can thus be described as a stochastic matrix with entries f (x|a) indexed by a ∈ A and x ∈ X. Parallel composition of two stochastic maps, f : A → X and g : B → Y , is just their tensor product f ⊗g : A⊗B → X ⊗Y , where A ⊗ B is the cartesian product of the underlying sets and one multiplies the probabilities in the formation of the tensor product. On the other hand, the sequential composition of f : A → X and h : X → Z to produce h • f : A → Z is given by the usual matrix multiplication. In the context of stochastic maps, it is also known as the Chapman-Kolmogorov equation.
In the string diagrammatic notation that we make heavy use of, objects are depicted as 'wires', while morphisms are generally drawn as 'boxes', with their domain below and their codomain above the box depicted as incident wires. Parallel and sequential composition is depicted by We depict morphisms m : I → X from the monoidal unit as X m with the interpretation being that they represent "random states". For example, in FinStoch these are the finitely supported probability measures, i.e. probability distributions.
Copying and discarding in FinStoch are likewise as one would expect. Specifically, copy X : X → X ⊗ X is a morphism that assigns, to each element x, the delta distribution δ (x,x) on the pair (x, x) ∈ X ⊗ X. Discarding, del X : X → I, is the stochastic map that corresponds to marginalization over X, where I denotes a fixed single-element set. Thus to each element of X, the stochastic map del X assigns the unique probability measure on I. Diagrammatically, we represent these maps as where we implicitly make use of X ⊗ I ∼ = X ∼ = I ⊗ X, so that I need not be drawn explicitly.
Abstracting these properties along with corresponding compatibility requirements leads to the notion of Markov category. For a more detailed discussion of the definition and its formal aspects, we refer the reader to [17]. A Markov category C is a symmetric monoidal category where the monoidal unit object I is a terminal object, 3 every object X ∈ C is equipped with distinguished morphisms copy X : X → X ⊗X and del X : X → I that make X into a commutative comonoid, and such that holds for all X, Y ∈ C.
Example 3.2. As far as this paper is concerned, the most relevant example is that of BorelStoch, which is the category of standard Borel spaces and measurable Markov kernels. It extends the objects of FinStoch by including both countably infinite measurable spaces as well as those isomorphic to [0, 1] with its Borel σalgebra. Morphisms coincide with those of FinStoch on finite sets, but in general they are given by Markov kernels. That is, a morphism f : A → X is specified by a family of probability measures f ( |a) over X, one for each a ∈ A, such that f (S| ) : A → [0, 1] is a measurable map for every measurable subset S ⊆ X. Sequential composition of Markov kernels f : A → X and h : X → Z is given by the Chapman-Kolmogorov equation as usual, which in our notation reads for every a ∈ A and every measurable T ⊆ Z. For more details, see [17,Section 4].

Conditionals.
In the introduction, we mentioned that one of the ingredients in our synthetic proof of de Finetti's Theorem is the existence of conditional probability distributions. Let us make this more precise in the context of Markov categories. In FinStoch, given a stochastic matrix f : whenever the denominator y ′ f (x, y ′ |a) is non-zero, and taking arbitrary values otherwise. This gives the corresponding probability of Y = y given that A and X attain values a and x, respectively. Equation (6) can be viewed as a version of Bayes' Theorem. One can also characterize f |X implicitly by which, unlike equation (6), can be expressed in string diagrams.
holds. We say that C has conditionals if such a conditional exists for all morphisms f : A → X ⊗ Y for any objects A, X, Y in C.
In BorelStoch, this amounts to the existence of regular conditional probabilities for measurable Markov kernels [18,Example 2.4].
As a special case of conditionals, we obtain a synthetic definition of a Bayesian inverse of f : A → X with respect to a prior m : I → A. with respect to X. Explicitly, it is a morphism f † : In general, one should keep in mind that even though we denote a Bayesian inverse of f by f † , it does depend non-trivially on the prior m. Moreover, conditionals and Bayesian inverses are generally not unique when they exist. In FinStoch, this is because f |X (y|x, a) is arbitrary whenever y f (x, y|a) = 0 in equation (7). However, one can show that conditionals (and therefore also Bayesian inverses) are unique up to almost sure equality [17, Proposition 13.6].
holds for all θ ∈ Θ and for all measurable subsets S of A and T of X respectively.

Representability.
Second on our list of proof ingredients is the ability to express a space of distributions on an object in a Markov category C as an object in C itself. For example, given an object X = {0, 1} in BorelStoch, we would like there be an object P X isomorphic to [0, 1] whose elements are themselves probability distributions over X. Indeed, BorelStoch allows for such a construction [18,Example 3.19]. However, this is not the case for FinStoch of course since P X cannot be a finite set. Before stating the general definition of P X more formally, we need to address the question of how to refer to "elements" of an object in a Markov category. After all, the objects do not come equipped with any underlying set a priori. In FinStoch, we can identify the finite set X with those morphisms I → X that are delta distributions. That is, they are morphisms describing no randomness the deterministic ones. More generally, deterministic morphisms in FinStoch are the {0, 1}-valued stochastic matrices. Intuitively, a deterministic f can be characterized by the fact that applying it to two independent copies of its input is guaranteed to result in the same pair of output values as applying f directly to the input and copying its output.
The subcategory of C that consists of its deterministic morphisms is denoted by C det .
Indeed, condition (14) fails for every stochastic matrix that is not {0, 1}-valued. Besides deterministic morphisms, we will also make use of the concept of m-almost surely deterministic ones.
Given Definition 3.6, we thus identify "elements" of the hypothetical space of distributions P X with deterministic morphisms I → P X. In order for these to faithfully represent probability distributions on X (and nothing else), in the general categorical setting we therefore require there to be a bijection between C(I, X) and C det (I, P X). Extending this requirement to morphisms with arbitrary domain A, which is expected to hold by the same reasoning, leads to the definition of distribution objects.

Definition 3.8 (representable Markov category [18, Definition 3.7])
. Given an object X in a Markov category C, a distribution object for X is an object P X together with natural bijections 4 between morphisms into X and deterministic morphisms into P X. Given any morphism f : A → X, we denote by f ♯ : A → P X its counterpart under this bijective correspondence. We say that C is representable if every object of C has a distribution object.
It turns out that a slightly stronger version of representability is needed in the synthetic proof of de Finetti's Theorem. In particular, we require that the identification from (16) is compatible with a.s.-equality in the following sense.
for all m : Θ → A and all f, g as indicated.
For example, BorelStoch is a.s.-compatibly representable [18,Example 3.19]. If we set A = P X in bijection (16), we get a correspondence between deterministic morphisms P X → P X and generic morphisms P X → X. The identity on P X corresponds to a map P X → X which we denote by samp, and which we can think of as taking a probability distribution p on X and returning a random element of X distributed according to p (hence, "sampling" from p). In BorelStoch, for instance, for every p ∈ P X and every measurable S ⊆ X we have By naturality of the bijection (16), for each morphism f : A → X we have that f = samp • f ♯ holds. For more details on this, see [18, Section 3].

Infinite Products.
The third and last ingredient that we need in the proof of our synthetic de Finetti's Theorem is the ability to construct countable products of objects. Once again we would not expect FinStoch to allow those, since its objects are merely finite sets, but BorelStoch does [19,Example 3.6]. The relevant definition is that of Kolmogorov products introduced in [19] in the context of 0/1laws for Markov categories. Given a hypothetical object X N describing the product of countably many copies of X, every probability measure f : I → X N should give rise to a corresponding measure f F : I → X F for each finite subset F ⊆ N. Intuitively, f F is given by marginalizing over those copies of X indexed by the set complement of F . Therefore, we might expect there to be a corresponding deterministic morphism π F : X N → X F , which gives f F when composed with f . Conversely, the Kolmogorov extension theorem suggests that one can reconstruct f uniquely from its family of finite marginals (f F ), provided that these are suitably compatible. That is to say, if F ′ ⊆ F is a further subset, then one can obtain f F ′ from f F by marginalizing over the extraneous copies of X. Under this condition, there should be a unique f such that f F = π F • f for all F .
The idea underlying Kolmogorov products is to turn these properties that one would expect from a countable product into a definition of a meaningful product of infinitely many objects in any Markov category. However, besides merely morphisms of type I → X N , we also require similar properties of those with a non-trivial domain A and an additional codomain Y that could be correlated with X N . Definition 3.10 (Kolmogorov powers [19,Definition 4.1]). Given an object X in a Markov category C, consider an object X N of C such that there is a natural bijection between • morphisms f in C(A, X N ⊗ Y ) and • families (f F : A → X F ⊗ Y ) of morphisms indexed by finite subsets F of N that are compatible in the sense that whenever F ′ is a subset of F , we have where π F,F ′ : X F → X F ′ acts as the identity on X F ′ and applies del X to each of the remaining factors, for all objects A and Y of C. If every morphism in the family (f F ) corresponding to the case of Y = I, A = X N , and f = id X N is deterministic, then X N is termed a countable Kolmogorov power of X.
For example, Kolmogorov's extension theorem (in the countable case) states that countable Kolmogorov powers exist in BorelStoch [19,Example 3.6].
Note that the family of morphisms that corresponds to id : X N → X N under the prescribed bijection is given by the "infinite marginalization maps" π F : X N → X F mentioned before, which play the role of product projections.
If the Kolmogorov powers X N and Y N exist for two objects X and Y , then for any morphism f : X → Y we get a canonical morphism X N → Y N as follows. First, for each finite subset F ⊂ N we form the map f F : X F → Y F as usual. The family of compositions for each F , by the bijection of Definition 3.10, corresponds to a unique morphism X N → Y N . We denote this morphism by f N . Although the original definition in [19] defines Kolmogorov products of any arbitrarily large family of objects, in the present context we limit ourselves to countable powers of one and the same object, since this is all we need for de Finetti's Theorem.
In the following sections, we use double wires in order to distinguish an object that is a countable Kolmogorov power (such as X N ) from a generic object of a Markov category (such as X) depicted by a single wire. See equation (20) for example. At times, we also use three dots to indicate a countable Kolmogorov power, such as in equation (21). The latter notation is motivated by the fact that a countable Kolmogorov power f N of a morphism f can be informally viewed as a countable number of parallel morphisms, each given by f .

De Finetti's Theorem for Markov Categories
Suppose that a Markov category C has countable Kolmogorov powers. We can then express what it means for a morphism with a countable power X N as codomain to be exchangeable. Note that for any injective function i : N → N (and in particular for any permutation) we can define a morphism X i : X N → X N that maps the n-th component in X N to • the i −1 (n)-th component of X N whenever n is in the image of i, and • discards it otherwise.
The construction of X i is by the definition of X N as the Kolmogorov power of X. That is, X i corresponds to the family of morphisms (X i F : X N → X F ) as in Definition 3.10, where X i F is the composite of the product projection π i(F ) : X N → X i(F ) with the canonical isomorphism X i(F ) ∼ = X F resulting from identifying the factors as prescribed by i.

Definition 4.1 (exchangeability). A morphism p :
A → X N is said to be exchangeable if it is invariant under finite permutations of the components of the Kolmogorov power X N . That is, we demand that for every finite permutation σ : N → N, we have Assumption 4.2. Unless stated otherwise, throughout the rest of this paper we assume that C is a Markov category that: (1) has conditionals, (2) is a.s.-compatibly representable, and (3) has countable Kolmogorov powers.
Note that Assumption 4.2 implies, in particular, that for every object X, the space (P X) N exists, and is equipped with a copy map (P X) N → (P X) N ⊗ (P X) N .
In particular, this result says that the outputs of p are conditionally independent and identically distributed. As we will see in the proof, the conditioning here is with respect to a synthetic version of the tail σ-algebra, thereby reproducing this classical aspect of de Finetti's Theorem as well. In fact, the proof uses an abstract version of the well-known result of measure-theoretic probability that the exchangeable σ-algebra and the tail σ-algebra coincide up to sets of measure zero [29,Corollary 12.18]. In the following synthetic version of this result, the role of these σ-algebras is played by all possible ways of "probing" joint distributions of X N by composing with a deterministic (or almost surely deterministic) morphism f . (1) Finite permutation invariance: For every finite permutation σ, we have (2) Shift invariance: For the successor function s : N → N mapping n to n + 1, The successor function can be equivalently defined as the inclusion of the second component in the coproduct decomposition N ∼ = 1 + N and we depict its action on the Kolmogorov power X N by either of the two following string diagrams: This morphism effectively discards the first component of X N .
Remark 4.6. While Theorem 4.4 captures the key part of de Finetti's Theorem characterizing exchangeable morphisms, we have not been able to prove that our assumptions imply the uniqueness of the "de Finetti measure" µ in equation (21). This property is often proven as part of classical versions of de Finetti's Theorem including the one of Hewitt and Savage for compact Hausdorff spaces [21].
Here is how we can use Theorem 4.4 to obtain the classical de Finetti's Theorem in the form of Theorem 2.1. First of all, we take as C the category BorelStoch, which satisfies the relevant assumptions. Moreover, since the usual statement is given for the case of probability measures as opposed to Markov kernels with nontrivial domain, it suffices to consider the case of A = I.
Then the left-hand side of equation (21) instantiated in our case is an exchangeable probability measure on X N in the sense of Section 2. Theorem 4.4 says that there exists a Markov kernel µ : I → P X (equivalently, a probability measure on P X) such that p can be written as in the right-hand side of equation (21). Evaluating this equation on a cylinder set corresponding to a sequence of measurable subsets S 1 , . . . , S n of X gives p(S 1 × · · · × S n ) = P X n i=1 P X samp(S i |q i ) copy(dq 1 ⊗ · · · ⊗ dq n |q) µ(dq) where we used the fact that samp(S|q) = q(S). Thus, Theorem 2.1 follows from Theorem 4.4.
Similarly, here is how Proposition 4.5 recovers the classical coincidence of exchangeable σ-algebra and tail σ-algebra up to null sets. In BorelStoch, a deterministic morphism f : X N → {0, 1} corresponds to an event in X N , and such f satisfies the shift invariance condition if and only if the corresponding event is, up to null sets, in the tail σ-algebra. Likewise, such f satisfies finite permutation invariance if and only if the event is, up to null sets, in the exchangeable σ-algebra.
Remark 4.7. Note that by making the same argument with A an arbitrary standard Borel space, one obtains a parametric version of the classical Theorem 2.1. It says that if the exchangeable probability measure p depends measurably on a parameter, then µ can also be chosen to depend measurably on the same parameter. This is the de Finetti theorem for exchangeable Markov kernels mentioned in the introduction.   [16] may be relevant here to establish the existence of conditionals.

Diagrammatic Proof of de Finetti's Theorem
The overall structure of the proof is presented in Figure 1. We first present a number of lemmas that may be useful in other contexts too. We assume throughout that we are in a Markov category C satisfying Assumption 4.2.
In the concrete setting of BorelStoch, this statement reads as follows in the case A = Y = I. Consider a probability measure p ∈ P (X N ) specifying an exchangeable joint distribution of infinitely many random variables. If we marginalize over the first component, then the resulting distribution is again p. In other words, if p is exchangeable, then it is also shift-invariant. More generally, even if we marginalize over any number of components whose indices are specified by the complement of the image of some injective function i : N → N, the resulting distribution is still p. The same logic can be applied in the presence of a non-trivial covariate Y and parameter A, i.e. when p is a Markov kernel A → Y ⊗ X N .
The relevant argument was essentially already given in the proof of [19, Section 5], but we reproduce the argument here in the present more general context. Note that this works the same way for any other infinite set in place of N (if the relevant Kolmogorov power exists).
Proof. Since X N is the Kolmogorov power of X, it suffices to prove equation (24) after composition with each of the infinite marginalization maps π F : X N → X F  where F is a finite subset of N as before. That is, we need to prove for each finite F ⊆ N. For any given i and F , we can find a finite permutation σ : N → N whose action on F coincides with that of i. By definitions of X σ and X i , this implies π F • X σ = π F • X i , and the claim now follows by the assumed finite permutation invariance.
The next lemma can be thought of as a synthetic statement about stochastic dynamical systems where t : Θ → Θ is the dynamics, p is an invariant probability measure, and f is an observable.
We can present the proof of Proposition 4.5 now. It is worth noting that neither Lemma 5.1 nor Lemma 5.2 use the assumption of representability of C. As expressed in the statement of Proposition 4.5, the following proof does not require representability either, even while making use of the previous two lemmas.
Proof of Proposition 4.5. Let us argue that shift invariance as expressed by equation (23) implies finite permutation invariance as expressed by equation (22). Indeed, for any finite permutation σ : N → N, there is an integer n σ beyond which all larger integers are fixed by σ. With s : N → N denoting the successor function introduced in the statement of Proposition 4.5, this entails σ • s nσ = s nσ . Therefore, we have (X s ) nσ • X σ = (X s ) nσ , where the morphism on the right-hand side effectively discards the first n σ components of X N . Thus, assuming shift invariance of f , we can infer the permutation invariance as follows: In particular, the first equality holds by exchangeability of p and because X σ −1 is a Bayesian inverse of X σ . The latter holds by virtue of the fact that X σ −1 is deterministic and the inverse of X σ . The second and fourth equations in (32) correspond to shift invariance of f applied n σ times, while the third is analogous to the first in reverse, using equation (31) in addition. Conversely, let us now assume finite permutation invariance of f and show that it implies shift invariance. By the first equality of (32), we have that the morphism p f In a sense, C A contains the same data as C; it is just organized differently. When composing morphisms in C A we use the composition of C and distribute a copy of A to each of the morphisms in the composition. The key aspect of the parametrization construction for our proof is that as long as C satisfies Assumption 4.2, so does the parametric category C A . The arguments for conditionals and a.s.-compatible representability have been presented in [18] as Lemma 2.10 and Lemma 3.22 respectively. Here, we also spell out the argument for Kolmogorov powers.
Lemma 5.5. If X N is a countable Kolmogorov power of X in C, then X N is also a countable Kolmogorov power of X in the parametric Markov category C A .
Proof. Let B, Y be arbitrary objects of C A . We have the following three bijective correspondences where the lower two are compatible families in the same sense as in Definition 3.10. The vertical one is natural in both B and X by assumption, while for the horizontal ones, naturality follows from the definition of C A .
Since identities in C A correspond to identities in C with A discarded, the infinite marginalization maps in C A are likewise given by discarding A and applying the respective π F ∈ C(X N , X F ). In particular, the infinite marginalization maps in C A are deterministic, which means that the countable Kolmogorov power of X in C A indeed exists and is given by X N . . This already has the desired form of equation (21). Now, for a general morphism p : A → X N , we apply this result to the parametric Markov category C A , in which p is represented by a morphism with domain I. By [18, Lemmas 2.10 and 3.22] and Lemma 5.5, C A satisfies our three assumptions provided that C itself does. As is mentioned in [18,Example 3.17], the sampling map in C A is represented by del A ⊗ samp in C. Therefore, instantiating equation