Reference A Domain Theory for Statistical Probabilistic Programming [vakar-kammar-staton-omega-qbs]

  • January 2, 2019
  • Matthijs Vákár, Ohad Kammar, Sam Staton
  • 10.1145/3290349

Abstract

  • January 2, 2019
  • Matthijs Vákár, Ohad Kammar, Sam Staton

We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixed-variance datatypes. Our semantics justifies important program equivalences including commutativity. Our new semantic model is based on `quasi-Borel predomains’. These are a mixture of chain-complete partial orders (cpos) and quasi-Borel spaces. Quasi-Borel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be commutative on any class of cpos with higher order functions. By contrast, quasi-Borel predomains do support both a commutative probabilistic powerdomain and higher-order functions. As we show, quasi-Borel predomains form both a model of Fiore’s axiomatic domain theory and a model of Kock’s synthetic measure theory. 

 @article
{vakar-kammar-staton-omega-qbs, title={A Domain Theory for Statistical Probabilistic Programming}, volume={3}, ISSN={2475-1421}, DOI={10.1145/3290349}, note={arXiv:1811.04196 [cs]}, number={POPL}, journal={Proceedings of the ACM on Programming Languages}, author={Vákár, Matthijs and Kammar, Ohad and Staton, Sam}, year={2019}, month={Jan}, pages={1–29} }

Backlinks

The Universal Property of Measure-Theoretic Probability [efr-AK18]

Introduction

Markov categories are an abstract approach to probability theory, which axiomatize the structure of categories of probability kernels, beyond the specific details of measure theory. They allow for abstract versions of a number of theorems of classical probability theory, from the 0-1 law of Kolmogorov Reference [rischel-fritz-infinite-products], the de Finetti theorem Reference [fritz-gonda-perrone-2021], and a version of the law of large numbers Reference [law-large-nums-fritz-etal]. They also provide an intuitive but rigorous graphical syntax for reasoning about probability.

In the same way that free Cartesian closed categories describe a minimal syntax for programming with higher-order functions (the simply typed lambda calculus), one may hope that free Markov categories of some sort may provide a minimal syntax for probabilistic programming. In the absence of generating morphisms, the free Markov category on a set of objects is identical with the free Cartesian category on the same set. Hence, although we can consider the free Markov category generated by some collection of primitive distributions, and view its morphisms as terms in a simple probabilistic programming language (Fritz and Liang Reference [fritz-liang-freemarkov-2023] have described the morphisms of this category as certain hypergraphs), the description of these terms as a free Markov category tells us nothing interesting about the equations between different probability distributions. This presents the following question: is there some additional structure on Markov categories such that the free such category has as its morphism probability kernels in the ordinary sense? In this case, the axioms of this structure would be suitable primitives for "simple" probabilistic programming.

It has been a subject of much speculation whether the "canonical" Markov categories can be described in terms of category theory directly, as a universal object of some kind. Fritz Reference [fritz-stochmat-2009] has given a presentation of \mathsf {FinStoch} (the Markov category of finite sets and stochastic matrices) by generators and relations, but this simply encodes the set of real numbers into the set of generators. Much more recently, Lorenzin and Zanasi Reference [lorenzin-zanasi-infinite-tensor-2025] have given a description of how to freely adjoin infinite tensor products to a Markov category, and shown that this presents a class of locally constant kernels. Chen Reference [chen-universal-stdborel-2019] has given a universal characterization of the Cartesian category of standard Borel spaces---thus leaving the question of characterizing the class of Markov kernels on top of this.

Chen's theorem is that the category of standard Borel spaces is initial among extensive, Boolean, countably complete categories (and functors which preserve finite coproducts and countable limits). Clearly \mathsf {BorelStoch} (or any other interesting Markov category) does not have countable limits, since it lacks products. The right notion of "countable completeness" for Markov categories is given by replacing the infinite products with Kolmogorov products, a notion introduced in Reference [rischel-fritz-infinite-products]. Similarly, the "extensive" and "Boolean" parts have to be modified (since we only expect deterministic maps into a coproduct to factor over a coproduct decomposition of the domain).

Beyond these modifications, as noted above, we need some extra structure to provide any nondeterministic morphisms at all. Perhaps the simplest such axiom would be to require the existence of a morphism I \to I + I, corresponding to a fair coinflip, subject to some equations describing its fairness. It turns out that such a morphism is necessarily unique if it exists, and thus this really becomes a property of, not additional structure on, a Markov category. This property, which we call a coinflip Markov category, seems to be about the minimal axiom you could expect to produce a reasonable probability theory.

With these ingredients, we can state our first theorem:

Theorem [efr-TVLB]

\mathsf {BorelStoch} is (bi-)initial among countably extensive, Boolean, coinflip Markov categories with countable Kolmogorov products. (And Markov functors which preserve countable coproducts, countable Kolmogorov products and pullbacks along deterministic monomorphisms).

A key inspiration for this theorem is Reference [escardo-simpson-universal-interval-2001], where Escardo and Simpson give a universal characterization of the interval [0,1] in terms of a "midpoint" operator which is analogous to our binary choice operator. To generate the non-dyadic real numbers they impose beyond basic algebraic properties of the midpoint operator an iterability axiom (see Definition [efr-JP37]), which ensures the existence of certain infinite sums. It turns out that in the presence of countable Kolmogorov products this assumption is unnecessary—however, using the iterability axiom, we can also give universal properties to the "discrete" Markov categories like \mathsf {FinStoch} (which lack these products).

Theorem [efr-FTTL]

Let \kappa be a regular cardinal. Let \mathsf {Set}_{\bar {\Delta }}^{< \kappa } denote the subcategory of \mathsf {Set}_{\bar {\Delta }} consisting of the sets of cardinality less than \kappa . Then \mathsf {Set}_{\bar {\Delta }}^{< \kappa } is the initial \kappa -distributive, externally iterable, coinflip Markov category. In particular, \mathsf {FinStoch} is the initial distributive, externally iterable, coinflip Markov category, and \mathsf {Set}_{\bar {\Delta }} is the initial small-distributive, externally iterable, coinflip Markov category.

(Here \bar {\Delta } denotes the countably supported probability distribution monad). In particular, \mathsf {FinStoch} is the initial (finitely) distributive, externally iterable, coinflip Markov category, and \mathsf {Set}_{\bar {\Delta }} is the intial small-distributive externally iterable coinflip Markov category.

Preliminaries [efr-8P2U]

The terminology Markov category was introduced by Fritz in Reference [fritz-synthetic-markov-cats], although the idea goes back to the work of Golubtsov, Reference [golubtsov-kleisli]. They have been developed extensively as an abstract foundation for probability theory, see eg Reference [fritz-gonda-perrone-rischel-rep], Reference [rischel-fritz-infinite-products], Reference [law-large-nums-fritz-etal], Reference [fritz-gonda-perrone-2021]. We now review the basics.

Definition Markov category

A Markov category \mathcal {C} is a symmetric monoidal category in which every object is equipped with a comonoid structure (X, \mathrm {copy}_X, \mathrm {del}_X), which is compatible with the monoidal structure in the sense that \mathrm {del}_{X \otimes Y} = \mathrm {del}_X \otimes \mathrm {del}_Y, \mathrm {copy}_{X \otimes Y} = (X \otimes \sigma _{X,Y} \otimes Y) \circ (\mathrm {copy}_X \otimes \mathrm {copy}_Y) and so that \mathrm {del}_X is a natural transformation.

There is a strictification result (Reference [fritz-synthetic-markov-cats], Theorem 10.17) for Markov categories which allows us to freely elide the structural isomorphisms—we generally do so throughout this paper.

The morphisms of a Markov category are thought of as probability kernels, that is functions with values in probability measures (where these terms may be interpreted in a suitably abstract sense). The copy and delete maps are the non-stochastic maps which either copy or delete their input.

It is simple to verify that every Markov category is semiCartesian, and thus the only choice involved in equipping a symmetric monoidal category with a Markov structure is \mathrm {copy}_X. A morphism f :X \to Y \in \mathcal {C} is called deterministic if it is a homomorphism for the given comonoid structure. The subcategory of deterministic morphisms is denoted \mathcal {C}_\mathrm {det} \subseteq \mathcal {C}. It is always a symmetric monoidal subcategory, and Cartesian. Conversely, every Cartesian category carries a unique Markov structure.

We will often use the notation of Cartesian categories and denote by \pi _A the map (A \otimes \mathrm {del}_B): A \otimes B \to A.

Given two maps f: X \to A, g: X \to B, there is a distinguished pairing X \to A \otimes B, given by (f \otimes g)\mathrm {copy}_X. This is called the independent pairing of f and g. Note that by naturality of \mathrm {del} and the comonoid equations, f and g can be recovered from this pairing by postcomposing with \pi _A or \pi _B. Thus "being independent" is a property of kernels with a tensor product as its codomain. We generalize this to higher tensor products in the obvious way.

The following class of examples captures almost all Markov categories of interest.

Example

If \mathcal {C} is Cartesian and P is a monoidal monad on \mathcal {C}, then the Kleisli category (which we denote \mathcal {C}_P) is a Markov category, with \mathrm {copy}_X being the diagonal in \mathcal {C}.

Definition

Let \mathcal {C},\mathcal {D} be Markov categories. An oplax Markov functor F: \mathcal {C} \to \mathcal {D} is an oplax symmetric monoidal functor so that the following diagram commutes:

An oplax Markov functor is strong if the underlying monoidal functor is strong.

The undecorated term Markov functor was defined in Reference [fritz-synthetic-markov-cats] to mean what we above called a strong Markov functor. From this point, "Markov functor" will always mean the strong notion.

Our goal in this paper is to construct certain functors between Markov categories. The following lemma is helpful in this regard.

Lemma

Let \mathcal {C}, \mathcal {D} be Markov categories and let F: \mathcal {C} \to \mathcal {D} be any functor. Then:

  1. F admits at most one oplax Markov structure, given by the independent pairing of the two projections F(\pi _X), F(\pi _Y): F(X \otimes Y) \to F(X), F(Y).
  2. This is a genuine oplax Markov structure if and only if F preserves deterministic and independent maps, in the sense that if X \to A \otimes B is independent, then F(X) \to F(A \otimes B) \to F(A) \otimes F(B) is independent.
  3. This oplax Markov structure is strong if and only if the restricted functor F_\mathrm {det} : \mathcal {C}_\mathrm {det} \to \mathcal {D}_\mathrm {det} preserves finite products.

Proof

It's straightforward to check that if F admits any oplax Markov structure, then it preserves deterministic maps and this restricts to an oplax monoidal structure on F_\mathrm {det} (the fact that the oplaxator itself must be deterministic follows from the associativity). But functors between Cartesian categories always admit a unique oplax monoidal structure. Hence any two oplax structures on F agree. The only obstruction to this oplax functor extending to a full Markov structure is that it may not be natural with respect to nondeterministic morphisms. Given X \to X', Y \to Y', the tensor X \otimes Y \to X' \otimes Y' is equal to the independent pairing of X \otimes Y \to X \to X' and the analagous map to Y'. Applying the assumptiong that F preserves independent pairings to this gives naturality. The converse is clear. Finally F is strong if F(X \otimes Y) \to F(X) \otimes F(Y) is an isomorphism, but this is exactly the claim that F_\mathrm {det} preserves products.

We denote by \mathsf {BorelStoch} the category of standard Borel spaces and Markov kernels (Reference [fritz-synthetic-markov-cats], Section 4). We denote by \mathsf {Borel} the category of standard Borel spaces and measurable maps. Note that \mathsf {Borel} = \mathsf {BorelStoch}_\mathrm {det}. Recall that the standard Borel spaces are those measurable spaces arising as the Borel \sigma -algebra on Polish spaces. By Kuratowski's theorem these are either discrete on a countable set, or isomorphic to the real numbers (in the Borel \sigma -algebra). Recall also that \mathsf {BorelStoch} is the Kleisli category of a monad on \mathsf {Borel} called the Giry monad, see Reference [giry-1982] (see also Reference [fritz-synthetic-markov-cats] section 4 for a review of the history of this concept).

The categorical notion of product extends obviously to define infinite products. Infinite products exist in many Markov categories of interest, such as those of measurable spaces and Markov kernels, but they clearly can't be characterized by their usual universal property. Instead, we can ask them to be Kolmogorov products, in the following sense:

Definition Infinite tensor products [efr-SIKM]

Let \mathcal {C} be a semiCartesian symmetric monoidal category and let \{X_j\}_{j \in J} be a family of objects. Then if P_f(J) denotes the set of finite subsets of J (ordered by inclusion), we obtain a diagram P_f(J)^\mathrm {op} \to \mathcal {C}, where F \mapsto \bigotimes _{j \in F} X_j, and the inclusion F \to F' is mapped to the morphism which applies the deletion X_j \to I for every j not in F.

An infinite tensor product of the collection \{X_j\} is a limit of the cofiltered diagram F \mapsto \bigotimes _{j \in F} X_j, if it exists and is preserved by the tensor Y \otimes - for every Y \in \mathcal {C}.

Definition Kolmogorov product [efr-EB3U]

Let \mathcal {C} be a Markov category. An infinite tensor product is called a Kolmogorov product if all the finite marginals \otimes _{j \in J} X_j \to \otimes _{j \in F} X_j are deterministic.

These were introduced in Reference [rischel-fritz-infinite-products], where it was also shown that \mathsf {BorelStoch} admits countable Kolmogorov products (Example 3.6).

Lemma [efr-OH6B]

Let \mathcal {C} be a Markov category. Then \mathcal {C} admits Kolmogorov products of a given cardinality \kappa if and only if \mathcal {C}_\mathrm {det} admits Cartesian products of the same cardinality, and the opfiltered limits of Definition [efr-SIKM] are preserved by the inclusion \mathcal {C}_\mathrm {det} \to \mathcal {C}

Note that given any Markov functor F: \mathcal {C} \to \mathcal {D}, and a family X_j so that the Kolmogorov product \bigotimes _j X_j exists, there is a family of (necessarily deterministic) maps F(\bigotimes _j X_j) \to \bigotimes _{j \in F} X_j for every finite F \subset J. As usual we say F preserves Kolmogorov products if this collection exhibits F(\bigotimes _j X_j) as the Kolmogorov product of the family F(X_j). If \mathcal {C}, \mathcal {D} admit Kolmogorov products of a given cardinality, F preserves them if and only if F_\mathrm {det} : \mathcal {C}_\mathrm {det} \to \mathcal {D}_\mathrm {det} preserves products of this cardinality.

When the family X is constant, we will denote the Kolmogorov product \bigotimes _{i \in J} X simply by X^J.

If \bigotimes _{i \in J} X_i is a Kolmogorov product and f_i: A \to X_i is a collection of kernels, there is a canonical independent coupling (f_i): A \to \bigotimes _i X_i, given as the limit of the finite independent couplings A \to \bigotimes _{i \in F} X_i. In the case where all f_i (and all the X_i) are equal, we will denote this simply as f^J : A \to X^J.

The Kolmogorov product (I + I)^\omega = 2^\omega will play an important role in this paper. We generally write 0,1 : I \to 2 for the two canonical points in 2. If b \in 2^\omega is an element, 0.b, 1.b, 001101.b \in 2^\omega denote the result of prepending the given string to b. We may also write 0.2^\omega instead of \{0\} \otimes 2^\omega for the subobject given by those streams starting with a 0, and so on.

Distributive and extensive Markov Categories [efr-MGSE]

We will need to impose a few different categorical properties on our Markov categories. These are analogues of preexisting properties of ordinary categories, but will typically need to be modified somewhat to suit Markov categories. The usual pattern is to demand that \mathcal {C}_\mathrm {det} has some property, and that this is preserved by the inclusion into \mathcal {C}. In this section we will describe these conditions.

For background on extensive and distributive categories, see Reference [carboni-lack-walters-extensive]. For background on Boolean categories, see Reference [johnstone-elephant-vol1], section A1.4. Reference [chen-universal-stdborel-2019] also contains a review of these terms and the relations between them that suffices for this paper.

The list of hypotheses we will chiefly be interested in is the following:

  1. \mathcal {C}_\mathrm {det} is Boolean, countably complete and (countably) extensive (so that it receives a unique functor from \mathsf {Borel} by Chen's theorem).
  2. The inclusion \mathcal {C}_\mathrm {det} \hookrightarrow \mathcal {C} preserves the countable coproducts, the pullbacks along coproduct inclusions (hence all monomorphisms), and carries the countable products to Kolmogorov products.

There are various ways we can break this up into sub-assumptions. For example, if \mathcal {C} admits Kolmogorov products of a given cardinality, \mathcal {C}_\mathrm {det} admits products of that cardinality. So if \mathcal {C} has countable Kolmogorov products and \mathcal {C}_\mathrm {det} has pullbacks along monomorphisms, \mathcal {C}_\mathrm {det} has all limits.

Remark

  1. In the Cartesian case, if \mathcal {C} is Boolean, countably complete and extensive, then it is also countably extensive (Reference [chen-universal-stdborel-2019], Lemma 2.5). However, the proof of this relies on identifying morphisms X \to Y with their graphs (subobjects of X \times Y), and applying our knowledge about the subobject lattice. In the Markov context, we can not necessarily identify a morphism with a deterministic subobject of X, hence this argument does not work—to be precise, \mathcal {C}_\mathrm {det} will have all countable coproducts but the inclusion will not necessarily preserve them. If \mathcal {C} is representable, the inclusion preserves all colimits and this limitation disappears.
  2. Let \mathcal {C}, \mathcal {D} be Markov categories with countable Kolmogorov products, so that \mathcal {C}_\mathrm {det}, \mathcal {D}_\mathrm {det} is countably extensive and Boolean, and the inclusions preserve the countable coproducts, and let F: \mathcal {C} \to \mathcal {D} be a strong Markov functor. Suppose F_\mathrm {det} : \mathcal {C}_\mathrm {det} \to \mathcal {D}_\mathrm {det} preserves countable limits and finite coproducts. Then it automatically preserves countable coproducts as well (again, by Chen's argument). Since these are also countable coproducts in \mathcal {C}, \mathcal {D}, it follows that F preserves countable coproducts as well.

Definition [efr-T0AU]

A Markov category is distributive (\kappa -distributive) if \mathcal {C}_\mathrm {det} admits finite (\kappa -small) coproducts, these are preserved by the inclusion \mathcal {C}_\mathrm {det} \hookrightarrow \mathcal {C}, and by the tensors A \otimes -.

In a distributive monoidal category, if A,B are each comonoids, then A+B acquires an induced comonoid structure given by A + B \to A \otimes A + B \otimes B \hookrightarrow (A+B)\otimes (A+B) If \mathcal {C} is a Markov category, each of these objects has furthermore a canonical given comonoid structure. \mathcal {C} is distributive as a Markov category if and only if the coproducts can be chosen so that the canonical comonoid structure coincides with the induced one.

This parametrization in a regular cardinal \kappa will recur a few times in this paper. We are chiefly interested in the cases \kappa = \omega , corresponding to finite coproducts, and \kappa = \omega _1, corresponding to countable coproducts (this case requires a weak form of the axiom of choice).

Definition Extensive Markov Category [efr-B2P7]

A Markov category is said to be an extensive Markov category if it admits finite coproducts, whose injections are deterministic, and which satisfy the following equivalent conditions:

  1. If we let \mathcal {C}_{/a}^\mathrm {det} refer to the full subcategory of the slice spanned by the deterministic morphism x \to a, we have an equivalence of categories \mathcal {C}_{/a}^\mathrm {det} \times \mathcal {C}_{/b}^\mathrm {det} \cong \mathcal {C}_{/a + b}^\mathrm {det}, given by taking coproducts
  2. \mathcal {C}_\mathrm {det} is an extensive category in the usual sense and the inclusion \mathcal {C}_\mathrm {det} \to \mathcal {C} preserves pullbacks along coproduct inclusions.

More generally, for an infinite regular cardinal \kappa , we say that \mathcal {C} is \kappa -extensive if \mathcal {C}_\mathrm {det} is a \kappa -extensive category in the ordinary sense and both coproduct inclusions and pullbacks along them are preserved by the functor \mathcal {C}_\mathrm {det} \to \mathcal {C}.

Note that any extensive Markov category is automatically distributive (for the same \kappa ). Note also that if \mathcal {C} is extensive Markov, then \mathcal {C}_\mathrm {det} automatically admits all finite limits, since it has finite products just by virtue of being a Markov category.

Recall that a coherent category is called Boolean if every subobject lattice is a Boolean algebra. Also note that an extensive category is Boolean (and coherent) as soon as it satisfies the condition that every monomorphism V \hookrightarrow X is a coproduct inclusion (the object V' so that A = V + V' is then the complement subobject of V). We will not need to study any other case than this, and so we simply make the following definition.

Definition Boolean Markov category [efr-7JNJ]

An extensive Markov category \mathcal {C} is Boolean (as a Markov category) if \mathcal {C}_\mathrm {det} is Boolean, i.e if every monomorphism in \mathcal {C}_\mathrm {det} is a coproduct inclusion.

In the common case that \mathcal {C} is the Kleisli category of a monad on \mathcal {C}_\mathrm {det}, the inclusion \mathcal {C}_\mathrm {det} \hookrightarrow \mathcal {C} automatically preserves all colimits, which makes many of the above things automatic.

Lemma [efr-198L]

Let \mathcal {C} be a representable Markov category, and let P be the associated distribution monad. Then

  1. If \mathcal {C}_\mathrm {det} is \kappa -extensive and P: \mathcal {C}_\mathrm {det} \to \mathcal {C}_\mathrm {det} preserves pullbacks along coproduct inclusions, then \mathcal {C} is \kappa -extensive.
  2. If \mathcal {C}_\mathrm {det} is Boolean, then \mathcal {C} is Boolean.
  3. If \mathcal {C}_\mathrm {det} is (finitely) extensive, Boolean, and \kappa -complete, and P: \mathcal {C}_\mathrm {det} \to \mathcal {C}_\mathrm {det} preserves the cofiltered limits \prod _{i \in J} A_i = \lim _{F \subseteq J \mathrm { finite}} \prod _{i \in F} A_i for |J| < \kappa , then \mathcal {C} is \kappa -extensive (and Boolean and admits \kappa -small Kolmogorov products).

Remark [efr-GZCD]

We will characterize \mathsf {BorelStoch} as the initial Markov category which is countably extensive, Boolean, admits countable Kolmogorov products, and a coinflip. Let us say a few words justifying these axioms as natural. Extensivity is a property of most categories of "spaces", and the requirement that \mathcal {C}_\mathrm {det} \hookrightarrow \mathcal {C} preserves coproducts and pullbacks along monomorphisms holds in essentially every Markov category of interest.

However, Boolean categories are a bit more uncommon. In the presence of extensivity, Boolean-ness is equivalent to I + I being a subobject classifier - the obstruction to this typically being that "the" indicator of many subobjects are discontinuous.

A common assumption about Markov categories is the presence of conditionals (Reference [fritz-synthetic-markov-cats] 11.5). If V \hookrightarrow X is a subobject, and I \to I + I, I \to V, I \to X are distributions of full support, then a Bayesian inverse of their pairing I + I \to X is forced to have a discontinuity at the boundary of V.

While this does not rise to the level of a formal argument that conditionals imply Boolean (it seems very hard to imagine such an argument, since conditionals are only defined up to almost sure equality, and measures with full support don't always exist, for example, in \mathsf {BorelStoch}), it does demonstrate the difficulties involved in admitting conditionals without being Boolean.

Proposition [efr-GY4W]

\mathsf {BorelStoch} is countably extensive and Boolean.

Proof

Note first that \mathsf {Borel} is countably extensive and Boolean, by Reference [chen-universal-stdborel-2019] theorem 1.1. Hence it suffices to observe that the Giry monad preserves pullbacks along coproduct inclusions. Consider X \to A + B. The claim is that the square

is a pullback, where X_A is the preimage of A inside X. But this is clear: a probability measure on A is exactly a probability measure on A + B which happens to be concentrated on A, and a probability measure on X has an image in G(A + B) of this form if and only if it is concentrated on X_A (and is such equivalent to a measure on X_A).

Midpoint algebras and Coinflips [efr-AHFX]

We will not have any hope of giving a universal property for \mathsf {BorelStoch}, or any interesting Markov category, without some property that forces certain maps to be nondeterministic. We now give such a structure. As mentioned, our basic idea will be to impose the existence of a "unbiased binary random choice". In a general Markov category, this choice forms a morphism A \otimes A \to A. The axioms that such a choice must satisfy are essentially the axioms described by Escardo and Simpson in Reference [escardo-simpson-universal-interval-2001], which they termed midpoint algebras. The main theorem of their paper is a characterization of the interval [0,1] as the free iterable (Definition [efr-JP37]) midpoint algebra on two points—this will play a central role in this paper.

Definition Midpoint algebra [efr-6W7X]

Let \mathcal {C} be a Cartesian category. Then a midpoint algebra is an object A equipped with m: A \times A \to A, so that: m(a,a) = a m(a,b) = m(b,a) m(m(a,b),m(c,d)) = m(m(a,c), m(b,d))

We will call a homomorphism of midpoint algebras (a morphism satisfying m(f(a),f(a')) = f(m(a,a'))) a midpoint homomorphism

Definition Internal midpoint algebra [efr-1XB5]

Let \mathcal {C} be any category. An internal midpoint algebra structure on an object A \in \mathcal {C} is a family of midpoint algebra structures on each \mathcal {C}(X,A), so that precomposition is a midpoint homomorphism for every f: Y \to X.

Note that if \mathcal {C} is Cartesian this agrees with the above definition.

Definition Coinflip structure [efr-QBVU]

Let \mathcal {C} be a Markov category. A coinflip structure is a internal midpoint algebra structure on each A \in \mathcal {C}, which is natural in A. In other words, it is a midpoint algebra structure on each homset \mathcal {C}(X,Y) so that both pre- and postcomposition are midpoint homomorphisms.

Proposition [efr-OX26]

Let \mathcal {C} be a Markov category. Then every coinflip structure on \mathcal {C} is equal.

Proof

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.

Definition Coinflip Markov Category [efr-VTCS]

A coinflip Markov category is a Markov category which admits a coinflip structure.

Note that any coinflip structure is determined by the family of maps m(\pi _0,\pi _1) : A \otimes A \to A. To define a coinflip structure, such a family \mu _A must satisfy the equations of a midpoint algebra, be natural in A, and have the further property that \mu _A f = \mu _A (\pi _0 f, \pi _1 f) (that is, the composite depends only on the projections of f).

Coinflip structures are not preserved by all Markov functors, since F(\mu _A) only has to enjoy the above property with respect to maps in the image of F. However, as we now show, this is true in the distributive case.

Definition Coinflip in a Markov category [efr-0XH9]

Let \mathcal {C} be a Markov category with finite coproducts. A coinflip in \mathcal {C} is a morphism f: I \to I + I obeying the following equations:

  1. Symmetry: \tau _{I,I} f = f, where \tau _{A,B} :A + B \to B + A is the canonical isomorphism.
  2. Interchange: (f + f)f = (I + \tau _{I,I} + I)(f + f)f

Given a coinflip in a distributive Markov category, there is a canonical induced natural transformation A \otimes A \to A, which makes every A \in \mathcal {C} into a midpoint algebra.

Proposition [efr-V3JG]

Let \mathcal {C} be a distributive Markov category. Any two coinflips in \mathcal {C} coincide. In particular, any Markov functor \mathcal {C} \to \mathcal {D} which preserves these finite coproducts also preserves the coinflip.

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.

Note that any coinflip I \to I + I in a distributive Markov category induces a coinflip structure, and vice versa. Since both notions are unique, this is obviously a 1-1 correspondence. From this we easily derive the following:

Corollary [efr-7QV9]

Let \mathcal {C}, \mathcal {D} be distributive coinflip Markov categories, and suppose F: \mathcal {C} \to \mathcal {D} is a Markov functor which preserves coproducts and the monoidal unit. Then F also preserves the coinflip structure.

The terminology "midpoint algebra" is from Reference [escardo-simpson-universal-interval-2001]. In that paper, Escardo and Simpson provide a characterization of the interval as the free midpoint algebra satisfying certain properties generated by two points. The key property is the following:

Escardo and Simpson introduced the following notion:

Definition Iterable midpoint algebra [efr-JP37]

A midpoint algebra (A,m) in \mathcal {C} is iterable if, for each s: X \to X \times A \in \mathcal {C}, there is a unique u : X \to A so that the diagram

If A is an internal midpoint algebra in a category \mathcal {C}, a priori, the only version of Definition [efr-JP37] we can impose is that all the midpoint algebras \mathcal {C}(X,A) are iterable (in \mathsf {Set}). However, if \mathcal {C} is Markov, we can alternatively demand the following (which is just Definition [efr-JP37] with tensor products instead of products):

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

In this case we might call u an iteration operator for s.

Definition [efr-Z9IU]

Let \mathcal {C} be a coinflip Markov category. Then it is called externally iterable if the midpoint algebras \mathcal {C}(X,Y) are all iterable in \mathsf {Set}. It is said to be internally iterable if they are all internally iterable.

Escardo and Simpson's theorem is that the set [0,1] is the free iterable, cancellative (i.e satisfying m(a,b) = m(a,c) \Rightarrow b = c) midpoint algebra on two generators. We now strengthen their theorem by proving that it is free among merely iterable midpoint algebras (since it cancellative, this implies their statement).

Lemma [efr-CZUI]

In \mathsf {Set}, the free iterable midpoint algebra on two generators 0,1 is [0,1]. That is, given an iterable midpoint algebra A and two points a_0, a_1, there exists a unique midpoint homomorphism f: [0,1] \to A so that f(0)=a_0, f(1)=a_1.

Proof

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.

Lemma [efr-JB06]

Let X be a possibly infinite set. Then the infinitary simplex \bar {\Delta }(X) = \{ (a_x \geq 0)_{x \in X} \mid \sum a_x = 1 \} is the free iterable midpoint algebra on X.

Proof

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.

Corollary [efr-REOY]

Any iterable midpoint algebra carries the structure of an algebra of \bar {\Delta }. Moreover any midpoint homomorphism between iterable midpoint algebras is a \bar {\Delta }-homomorphism. In particular, if \mathcal {C} is an externally iterable coinflip Markov category, each homset \mathcal {C}(X,Y) is a \bar {\Delta }-algebra, and composition is biconvex (i.e convex in each variable separately). If \mathcal {C} \to \mathcal {D} is a functor between externally iterable coinflip Markov categories which preserves the coinflip (eg if \mathcal {C}, \mathcal {D} are distributive), it automatically preserves this structure.

The situation with coinflip Markov categories is similar to the situation of preadditive categories, known for example from the study of homological algebra. Under mild conditions on a category (admitting finite products and coproducts is sufficient), an enrichment over commutative monoids is unique if it exists.

Proposition [efr-E4WU]

Let \mathcal {C} be a coinflip Markov category. If it is externally iterable, then it is internally iterable.

Proof

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.

Proposition [efr-60YW]

Let \mathcal {C} be a coinflip Markov category which is countably distributive. If \mathcal {C} is internally iterable, then it is externally iterable.

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.

If the Markov category under consideration has at least countable coproducts, we may therefore simply speak of an iterable coinflip Markov category.

The universal property of discrete probability [efr-ALKX]

Using our description of the free iterable midpoint algebras, we can now prove Theorem [efr-FTTL].

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.

We can also describe the free iterable coinflip Markov category on a generic category, as follows:

Proposition

Let \mathcal {C} be a Markov category. Let \bar {\Delta } (\mathcal {C}) denote the category with the same objects, whose homsets are given by \bar {\Delta } (\mathcal {C}(X,Y)), with the uniquely extended bilinear composition. Then \bar {\Delta } \mathcal {C} is a Markov category, and \mathcal {C} \hookrightarrow \bar {\Delta } \mathcal {C} presents it as the free externally iterable coinflip Markov category generated by \mathcal {C}

Note that, although coinflip structures are unique, not every functor preserves them. Hence the free coinflip Markov category on a category which is already coinflip is not the category itself, as one might expect. It is interesting to consider whether a version of this theorem for distributive Markov categories exists (which would generalize Theorem [efr-FTTL]), but we do not currently know how to prove such a theorem.

The universal property of \mathsf {BorelStoch} [efr-D09F]

We are now ready to prove Theorem [efr-TVLB]. The basic point is that any Markov kernel between standard Borel spaces can be written as the composite of a measurable function f: A \times 2^\omega \to B with the uniform measure on c^\omega : I \to 2^\omega . By Chen's theorem, the image of f is uniquely determined, and by Proposition [efr-V3JG], so is the image of c^\omega . Hence there is at most one such functor---what we need to prove is that the above is well-defined (that is, choosing different factorizations gives the same kernel in the image) and actually forms a Markov functor.

The strategy for the proof is as follows:

  1. Observe that for any \mathcal {C}, there is an essentially unique functor \mathsf {Borel} \to \mathcal {C} (which lands in \mathcal {C}_\mathrm {det}), by Chen's theorem.
  2. Prove that there is a (Markov) extension to the category of discrete kernels, \mathsf {Borel}_{\bar {\Delta }}.
  3. Finally prove that there is a further Markov extension to \mathsf {BorelStoch}

We have essentially already given the proof of the first step in the introduction, but let us state it here for completeness.

Proposition [efr-AFCK]

Let \mathcal {C} be a Markov category which is countably extensive, Boolean, coinflip, and admits countable Kolmogorov products. Then there is an essentially unique (strong) Markov functor i: \mathsf {Borel} \to \mathcal {C} which preserves pullbacks along monomorphisms and countable Kolmogorov products.

Proof

Since \mathsf {Borel} is Cartesian, any such Markov functor must factor over \mathcal {C}_\mathrm {det}. \mathcal {C}_\mathrm {det} has countable limits (it has countable products by Lemma [efr-OH6B] and pullbacks along monomorphisms, which along with finite products suffices to build equalizers) and is countably extensive and Boolean by assumption. The assumptions on i are equivalent to the factorization \mathsf {Borel} \to \mathcal {C}_\mathrm {det} preserving countable limits and countable coproducts. Hence this uniqueness is exactly Reference [chen-universal-stdborel-2019] theorem 1.1

To make our results slightly more broadly applicable, since there aren't many Boolean categories, we will instead take a suitable Markov functor \mathsf {Borel} \to \mathcal {C} as the input, and prove that given such, there is a unique extension of the above kind. In the below, we will generally abuse notation and identify a standard Borel space with its image under this functor.

Let's now see the details of part 2. We begin with the following lemma, which is what allows us to use infinitary sampling without the iterability assumption.

Lemma [efr-K4NK]

Let \mathcal {C} be an extensive coinflip Markov category with countable Kolmogorov products, and let \mathsf {Borel} \to \mathcal {C} be a strong Markov functor which preserves pullbacks along coproduct inclusions and countable Kolmogorov products. Let V_1 \subseteq 2^\omega be the subobject consisting of those sequences containing infinitely many ones. Then the map c^\omega : I \to 2^\omega factors over V_1. In particular, it factors over the inclusion 1 . 2^\omega \sqcup 01.2^\omega \sqcup \cdots \hookrightarrow 2^\omega of the subobject of sequences with at least one 1.

Proof

Let r_1: 2^\omega \to 2 be the indicator of the subset consisting of those streams which have only finitely many 1s. Observe that for any finite N, r_1 factors over the second coordinate of the decomposition 2^\omega \to 2^N \times 2^\omega .

As a result, if we form the joint I \to 2^\omega \otimes 2 given by sampling the uniform distribution and computing r_1, the second coordinate is independent of any finite prefix of the first. Hence, by the abstract Kolmogorov zero-one law (Reference [rischel-fritz-infinite-products], theorem 5.3), the composite r_1 c^\omega : I \to I+I is deterministic.

Hence it classifies some subterminal object q. By symmetry, r_0 c^\omega is the indicator of q as well, where r_0 is the indicator of sequences with only finite many 0s. But these two subterminal objects must be disjoint, hence they must both be empty. (This step uses the fact that pullbacks along monomorphisms in \mathcal {C}_\mathrm {det} are still pullbacks in \mathcal {C})

So r_0c^\omega , r_1c^\omega are both equal to 0 : I \to 2. It follows that c^\omega factors over the subobject 2^\omega \setminus \{0\}^\omega \hookrightarrow 2^\omega (since any sequence with finitely many zeroes certainly has at least one 1).

Thus we can define a countable-arity operator M_A: A^\omega \to A in any of these categories by drawing a sample from c^\omega \in 2^\omega and projecting onto the coordinate of the first 1 (which necessarily exists).

For any standard Borel space A, let BT(A) denote the (again standard Borel) space of balanced, finite binary trees with leaves labeled by A. This can be identified with the coproduct \sum _{n \in \mathbb {N}} A^{2^n}. Let g : BT(A) \times BT(A) \to BT(A) glue two trees together, duplicating the shallower one so that they have the same depth. In \mathcal {C}, there is a unique kernel BT(A) \to A which carries this operation to the midpoint operation in \mathcal {C}. Note that this can be factored as a map BT(A) \times 2^\omega \to A which uses the first n bits to choose a branch, composed with the uniform distribution.

Given anything like (BT(A)^{\omega \times \omega })^{\omega }, we can build a well-defined map into A by composing these sampling homomorphisms. This is what we mean below by a sentence like "the sampling homomorphism BT(A)^{\omega ^N} \to A. Note that this is well-defined in any extensive, coinflip \mathcal {C} with countable Kolmogorov products equipped with \mathsf {Borel} \to \mathcal {C}.

Note that we have not proven that M_A is uniquely determined by the coinductive definition M_A(a_1, \dots ) = m(a_1, M(a_2, \dots )), merely constructed a canonical such operation. We have not been able to prove uniqueness in general (which would imply that any countably distributive, Boolean, countably complete coinflip Markov category is iterable), but neither do we know of a counterexample.

Lemma [efr-X0VA]

With \mathcal {C}, \mathsf {Borel} \to \mathcal {C} as above, let A be (the image of) a standard Borel space, and consider the map \lambda : (BT(A)^\omega )^\omega \to A given by sampling two natural numbers according to c^\omega : I \to 2^\omega \setminus 0 \to \omega and indexing with them, then using the canonical sampling map. There exists a map BT(A)^{\omega \times \omega } \to BT(A)^\omega which preserves the sampling map. Moreover this map also preserves the map into \Delta (A).

Proof

Let F: BT(A)^{\omega \times \omega } \times (2^\omega \setminus 0)^2 \times (2^\omega )^\omega \to A be a parametrization of the sampling map. Specifically, the first two bitstreams select the indexes (i,j) into the matrix of finitary distributions, after which the ith of the remaining bitstreams is used to choose a branch.

Let us adopt the convention that the first index chooses the column and the second index chooses the row when describing the manipulations below.

Given a sequence (d_{ij}) \in BT(A)^{\omega \times \omega }, construct r_1(d)_{ij} as follows:

  1. r_1(d)_{1j} = g(d_{11}, g(d_{12}, d_{21}))
  2. r_1(d)_{2j} = g(d_{1(j+2)},d_{2(j+1)})
  3. r_1(d)_{ij} = d_ij for i \geq 3

First note that clearly r_1(d) has the same image in \Delta (A) as d—the first column of r_1(d) has the same sum as the three most probably indices of d, and the second column of r_1(d) has the same sum as the remainder of the first two columns of d. Also note that there exists a permutation \rho _1 : (2^\omega \setminus 0 )^2 \times (2^\omega )^omega \to (2^\omega \setminus 0)^2 \times (2^\omega )^omega so that F(r_1(d),\rho _1(b)) = F(d,b).

\rho _1(b_1,b_2,(b_3^i)) can be chosen as follows: it does not modify b_3^i for i>2 (since these bits are only used for choices in the first column). Omitting therefore these strings from the notation below, we define \rho _1(1.c,1.r,s^1,s^2) = (1.c,r,1.s^1,s^2) \rho _1(1.c,01.r,s^1,s^2) = (1.c, r,01.s^1,s^2) \rho _1(01.c,1.r,s^1,s^2) = (1.c,r,10.s^2, s^1) \rho _1(1.c, 00.r, s^1,s^2) = (01.c, r, s^2, 1.s^1) \rho _1(01.c, 0.r, s^1,s^2) = (01.c, r, s^1, 0.s^2) \rho _1(00.c,r,s^1,s^2) = (00.c,r,s^1,s^2)

It is straightforward to verify that \rho _1 is well-defined, that F(r_1(d),\rho _1(b)) = F(d,b) as required. Moreover we see that every finite projection of the output of \rho _1 factors over some finite prefix of the input, and that the resulting maps 2^N \to 2^M carry the uniform distribution to the uniform distribution. This implies that \rho _1 c^\omega = c^\omega .

r_1 "flattens" the first column of d. Now we can apply r_1 again to the remaining columns to flatten the second column, and similarly apply \rho _1 ignoring the first bit of c and s^1 to obtain a corresponding permutation. Let r_N, \rho _N be the map an permutation that flatten the first N columns. Note that by construction each output bit of r_N is eventually stable for high N, and the same is true for \rho _N. Let r_\infty , \rho _\infty be the limiting maps.

Then when the first 1 in the part of \rho _\infty (b) which selects the i appears before index N, F(r_\infty (d),\rho _\infty (b)) depends only on the first N rows, hence is equal to F(r_N(d),\rho _\infty (b)), which is then equal to F(d,b). Since \rho _\infty is the limit of permutations, it preserves the uniform measure, and so the composite F(d,c^\omega ) = F(r_\infty (d), \rho _\infty (c^\omega )) = F(r_\infty (d), c^\omega ).

This proves that r_\infty preserves the sampling map. But clearly r_\infty factors over the inclusion of BT(A)^\omega \hookrightarrow BT(A)^{\omega \times \omega } as the "flat" sequences of sequences, and equally clearly this inclusion preserves the sampling map. This concludes the proof.

Lemma [efr-HYFI]

Let \mathcal {C} be an extensive Markov category with countable Kolmogorov products. Let \mathsf {Borel} \to \mathcal {C} be a Markov functor which preserves countable coproducts, countable Kolmogorov products and pullbacks along coproduct inclusions. Then:

  1. For every n, the iterated sampling operator BT(A)^{\omega ^n} \to A factors over the map BT(A)^{\omega ^n} \to \bar {\Delta }(A).
  2. The composite map \coprod _n BT(A)^{\omega ^n} \to \Delta (A) is a split epimorphism, and thus the factorization is unique, giving a well-defined sampling map s_A: \Delta (A) \to A for every standard Borel space A.
  3. This sampling map is a \omega -midpoint homomorphism, in the sense that s_A(\sum _i 1/2^i \mu _i) = M_A(s_A \mu _1, s_A \mu _2, \dots ).
  4. These maps assemble into a functor \mathsf {Borel}_{\bar {\Delta }} \to \mathcal {C} which extends the unique \mathsf {Borel} \to \mathcal {C}.

Proof

By Lemma [efr-X0VA], we see that we can immediately flatten any nested sequence in BT(A)^{\omega ^n} into a sequence of dyadic binary trees in BT(A)^\omega , without altering either the sampling map or the represented distribution in \bar {\Delta (A)}. Hence it suffices to prove that the sampling map BT(A)^\omega \to A factors over \bar {\Delta (A)}.

It is clear that the sum map BT(A)^\omega \to \bar {\Delta }(A) is surjective. We will begin by choosing a particular splitting of this map, assigning to each countably supported measure a "normal form" in BT(A)^\omega

Fix an arbitrary total ordering on A. If A is countable there is no difficulty doing this, if A = 2^\omega , we may use the lexical ordering.

Given a finitary distribution \mu , we compute its normal form as follows:

  1. Let N_0 be the smallest natural so that there exists a dyadic distribution \nu _0 = \sum _i \frac {k_i}{2^N} a_i so that \frac {1}{2}\nu _0 < \mu - that is, for every element of A, the probability under \frac {1}{2}\nu _0 is strictly less than the probability under \mu .
  2. Let \nu _0 be a dyadic distribution as above, choosing the lowest possible a_i according to the chosen ordering. Represent \nu _0 as a balanced binary tree of minimal depth, with the leaves increasing left to right.
  3. Repeat these steps with \mu - \frac {1}{2}\nu _0 to construct \nu _1, \nu _2, \dots .

It is clear that this defines a measurable map \Delta (A) \to BT(A)^\omega , and that this is a section of the map \sum _i 1/2^i \nu _i in the other direction.

  1. Let S: BT(A)^\omega \times (2^{\omega } \setminus 0) \times (2^\omega )^\omega \to A be the sampling map, which uses the first bitstream to choose the index i from the sequence, then the ith one of the remaining streams to sample from the given binary tree.
  2. Note that by construction, if \nu _1 is the first element in the normal form of \mu , and \lambda _i is another sequence of binary trees so that \sum _i 1/2^i \lambda _i is equal to \mu , then there exists some finite prefix so that 1/2 \nu _0 < \sum _{i=0}^N 1/2^i \lambda _i. Then there exists some rearrangement of this prefix \lambda _i' so that \lambda _1' = \nu _1 (and \lambda '_i = \lambda _i when i>N). Let \mathrm {nm}_k: BT(A)^\omega \to BT(A)^\omega be the map which puts the first k elements into the normal form like this. Note that for each k there exists some permutation \sigma _k : BT(A)^\omega \times (2^{\omega } \setminus 0) \times (2^\omega )^\omega \to (2^{\omega } \setminus 0) \times (2^\omega )^\omega which, for each possible sequence, witnesses this rearrangement (in the same way as Lemma [efr-X0VA]).
  3. By construction the nth coordinate of \mathrm {nm}_k(a) is equal for all k > n, and so there is a well-defined limiting map \mathrm {nm}_\infty : BT(A)^\omega \to BT(A)^\omega , which (by construction) carries a sequence to its normal form.
  4. For \sigma _k, similarly note that the first n bits (deciding the index into the sequence) are fixed for k > n, and the same is true for the n first streams used to sample from the given binary trees.
  5. Let \mathrm {nm}_\infty and \sigma _\infty be the limiting maps.

Now observe that F(a,b) = F(\mathrm {nm}_\infty (a),\sigma _\infty (a,b)), and that \sigma _\infty (a,b) for each a preseves the uniform measure. Hence just as before, this proves that the sampling map commutes with taking the normal form, as we wanted.

Observe that (for any monad), the Kleisli category is presented by adding morphisms s_A: TA \to A for each A, subject to the equations s_A\eta _A = 1_A and s_A s_{TA} = s_A \mu _A. We have just constructed the s_A, so we now have to prove that they satisfy these equations. Unitality is clear. The multiplicativity condition follows by observing that any finitary distribution on \Delta (A) can be decomposed as an iterated sum coming from \Delta (A)^{\omega ^N}, at which point this reduces to the mentioned \omega -midpoint homomorphism property.

We are now ready for the final step, to construct the extension of the functor \mathsf {Borel}_{\bar {\Delta }} \to \mathcal {C} over \mathsf {Borel}_{\bar {\Delta }} \hookrightarrow \mathsf {BorelStoch}

Lemma [efr-JK8U]

Let \phi : A \to (2^\omega )^k be a kernel in \mathsf {BorelStoch}, and let \vee ^k : (2^\omega )^k \to 2^k be the map which is 1 in each coordinate if the corresponding sequence contains at least one 1 (and zero else). Let \mathsf {Borel} \to \mathcal {C} be as above, and let F: \mathsf {Borel}_{\bar {\Delta }} \to \mathcal {C} be the unique extensions of Lemma [efr-HYFI]. Write \bar {F}(\phi ) for the unique map F(A) \to F((2^\omega )^k) given as the limit of F applied to the finite truncations. Then F(\vee ^k)\bar {F}(\phi ) = F(\vee ^k \phi )

Proof

We proceed by induction on k, the case k=0 being trivial.

First, consider a kernel \alpha : A \to (2^\omega )^k which, on the first N bits in the first coordinate, is concentrated on a given string a = a_1,\dots a_N which contains at least one 1. This kernel factors over the inclusion of this component: (2^\omega )^k = \{a\} \otimes 2^{\{N+1, \dots \}} \otimes (2^\omega )^{k-1} \sqcup (2^N \setminus \{a\}) \otimes 2^{\{N+1, \dots \}} \otimes (2^\omega )^{k-1}

This factorization is preserved by F (which preserves coproducts). Note that \vee ^k, when restricted to this summand, factors over the projection (2^\omega )^k \to (2^\omega )^{k-1}. So we can write F(\vee ^k)\bar {F}(\alpha ) = F((1,\vee ^{k-1}) \pi )\bar {F}(\alpha ). It is clear that F(\pi )\bar {F}(\alpha ) = \bar {F}(\pi \alpha ), and so by induction this means F(\vee ^k)\bar {F}(\alpha ) = F(\vee ^k \alpha ).

By an analogous argument (without passing through the finite truncation), if \alpha is concentrated on the string 0 \in 2^\omega in the first coordinate, again F(\vee ^k)\bar {F}(\alpha ) = F(\vee ^k \alpha )

Now consider the generic kernel \phi of the lemma. Let A = A_0 \sqcup A_1, where A_0 consists of those a for which the probability that the first coordinate is zero is \geq 1/2, and A_1 is the complement, consisting of those for which at least one 1 has probability >1/2. Note that by \sigma -continuity, there exists for each a \in A_1 some N_a so that there is a probability \geq 1/2 of an 1 in the first N_a coordinates. Note that the least such N_a is a measurable function of a, and so A_1 decomposes into a sum A_1 = A_1^1 \sqcup A_1^2 \dots , where on A_1^N there is a \geq 1/2 probability of an 1 in the first N coordinates.

Now let \mu _1 be the kernel defined as follows:

  1. On A_0, it is deterministically 0 in the first coordinate, and given by the conditional distribution given this in the last k coordinates.
  2. For a \in A_1^N, choose some distribution \nu on 2^N so that \nu / 2 is less than the marginals of \phi , and so that \nu is concentrated away from 0 (this is possible by construction of A_1^N). Then for each b \in 2^N, let \xi _b be the measure which is concentrated on that bitstring on the first N bits, and given by the conditional distribution according to \phi everywhere else. Let \mu _1(a) = \sum _{b\in 2^N} \nu (b) \xi _b

Observe that by construction, \mu _{1/2} \leq \phi . Now we can continue the recursion, defining \mu _2, \mu _3, \dots , and we must necessarily have \sum _i 1/2^i \mu _i = \phi . This sum must be preserved by \bar {F} (where the meaning of this sum in \mathcal {C} is given by the canonical sampling morphism X^\omega \to X, or equivalently by the dual I \to \omega ). Therefore we have F(\vee ^k)\bar {F}(\phi ) = F(\vee ^k)(\sum _i 1/2^i \bar {F}(\mu _i)) = \sum _i 1/2^i F(\vee ^k) \bar {F}(\mu _i) = \sum _i 1/2^i F(\vee ^k \mu _i) = F(\vee ^k \phi ), finishing the proof.

Lemma [efr-D3QE]

Let \mathsf {Borel} \to \mathcal {C} be as above. Then it admits a unique extension to \mathsf {BorelStoch} \to \mathcal {C}.

Proof

Using Lemma [efr-VH33], there is a unique extension F: \mathsf {Borel}_{\bar {\Delta }} \to \mathcal {C}. There is a faithful (identity on objects) functor \mathsf {Borel}_{\bar {\Delta }} \to \mathsf {BorelStoch} - the only case where this is not full is \operatorname {\mathrm {Hom}}(A,2^\omega ).

It is apparent that we must extend this functor by defining \bar {F}(\phi : A \to 2^\omega ) = \lim _n F(\pi _{2^n}\phi ), using the universal property of F(2^\omega ) = F(2)^\omega . It is apparent that this preserves independent pairings—the only question is whether this extension is actually functorial. By the limit property it suffices to prove that it is functorial for any composable pair A \xrightarrow {\phi } 2^\omega \xrightarrow {\psi } K with K finite.

Let a function f: 2^\omega \to K be good if \bar {F}(\phi ) ; F(f) = F(\phi ; f) for all kernels \phi : A \to 2^\omega (for all A). Let an algebra of sets \mathbb {A} \subseteq \mathcal {B}(2^\omega ) (i.e a collection of subsets stable under finite unions and complements) be called good if every \mathbb {A}-measurable map 2^\omega \to K to a finite set is good. Now we claim:

  1. The class \mathbb {A}_0 of sets of the form V \times 2^\omega for V \subseteq 2^N, N finite, is a good algebra.
  2. If \mathbb {A} is a good algebra, let \mathbb {A}^+ be the smallest algebra containing all countable unions of sets in \mathbb {A}. Then \mathbb {A}^+ is again a good algebra.
  3. Any directed union of good algebras \mathbb {A}_0 \subseteq \mathbb {A}_1 \dots \subseteq A_\alpha \subseteq is again a good algebra.

First note that, by Zorn's lemma, this straightforwardly implies the full Borel \sigma -algebra is a good algebra, which in turn concludes the proof.

Point 3 holds, since both being an algebra and being good are finitary properties (any map to a finite set which is measurable for the union must be measurable at some finite stage). Point 1 is a straightforward consequence of the fact that the projections 2^\omega \to 2^N are good by construction. So we are left with point 2.

Let \mathbb {A} be a good algebra. Let us identify sets by their indicators 2^\omega \to 2. Then we can write any set in \mathbb {A}^+ as g(\vee (f_1^i(-)), \vee f_2^i(-), \dots , \vee f_k^i(-)), where g: 2^k \to 2 is some function, \vee : 2^\omega \to 2 is the indicator of the sequences with at least one 1, and f_j^i, 0 \leq j \leq k, 0 \leq i < \infty are a bunch of \mathbb {A}-measurable functions.

By assumption the pairing of all the f's, 2^\omega \to (2^\omega )^k is good, and so it suffices to show that the mapping (\vee )^k : (2^\omega )^k \to 2^k is good. By induction we may suppose this holds for (\vee )^{k-1}, since it is trivial for k=0.

Now let \phi : A \to (2^\omega )^k be some kernel. Write A = A_0 + A_1, where A_0 is the subset where the probability of only zeroes in the first stream is at least 1/2, and A_1 is the complement, where the probability of at least one 1 in the first stream is >1/2. Observe that by \sigma -continuity, for each a there must be some N so that the probability of at least one 1 in the first N elements of the first stream is at least 1/2. Decompose A_1 into A_1^1 + A_1^2 + \cdots , where for a \in A_1^N there is at least a 1/2 probability of the first 1 being before N. Let \psi _1 : A \to (2^\omega )^k be a kernel which on A_0 is given by (0, \otimes \mu _{2\dots k}) where \mu _{2,\dots k} is the kernel giving the conditional distribution of the remaining streams if the first stream is 0. On A_1^N, it is given by a linear combination \sum _{s \in 2^N \setminus 0} \delta _{s} \otimes \mu _s, where \mu _s is the conditional distribution of the rest of the stream and the remaining streams - we choose this linear combination so that 1/2 of it is \leq the actual probability of each of those prefixes.

Thus we obtain a decomposition of \phi as \sum _i \frac {1}{2^i} \phi _i where for each \phi _i, the distribution on the first coordinate is either concentrated on 0 \in 2^\omega , or concentrated away from 0 on some finite prefix. Each of these satisfy F(\vee ^k)\bar {F}(\phi _i) = F(\vee ^k \phi _i). Hence, since F(\vee ^k) must preserve the infinite linear combination, \vee ^k must be good as desired.

Now let f: 2^\omega \to B be a kernel, and let \phi : A \to 2^\omega again be a kernel. We can factor f as a measurable map \bar {f} : 2^\omega \times 2^\omega \to B, composed with the uniform c^\omega : I \to 2^\omega . By the above we have F(f) = F(\bar {f})\circ (F(c^\omega ) \otimes 2^\omega ). By monoidality, it follows that \bar {F}(f)\bar {F}(\phi ) = F(f\phi ) as desired.

Now Theorem [efr-TVLB] follows trivially from Proposition [efr-AFCK]

Instead of studying Markov categories, one could study probability monads. The relevant question would then have been to give a universal property for the Giry monad. Our theorem implies this immediately:

Corollary

Let T be a bicommutative, affine monad on \mathsf {Borel} so that T(2) contains a coinflip, T preserves the limits \lim _{F \subset J \mathrm { F finite}} \prod _{i \in F} X_i and pullbacks along coproduct inclusions, and the induced midpoint algebras on TX are all iterable. Then there is a unique monoidal monad homomorphism G \to T, where G is the Giry monad.

Proof

Subject to these assumptions, \mathsf {Borel}_T is a Markov category which satisfies the hypotheses of Theorem [efr-TVLB]. Hence there is a strong monoidal, identity-on-objects functor \mathsf {BorelStoch} = \mathsf {Borel}_G \to \mathsf {Borel}_T. Such functors correspond bijectively to morphisms of monads G \to T (see eg Reference [barr-wells-triples-2005], Theorem 3.6.3), finishing the proof.

This settles an unpublished

Further work

Not all interesting measurable spaces are standard Borel. A simple example is the uncountable product \prod _{t \in \mathbb {R}} \mathbb {R}, classifying general stochastic processes valued in \mathbb {R} (although note that many important subsets of this, such as the space of continuous stochastic processes, are standard Borel). It would be interesting to look for a generalization of this work to a larger class of measurable spaces, or alternatively to describe in some other terms the initial coinflip Markov category which is \kappa -extensive, Boolean and admits \kappa -small Kolmogorov products for larger \kappa .

The results of Reference [chen-universal-stdborel-2019] actually provides the deterministic version of this for all \kappa : the initial \kappa -complete, (\kappa -) extensive, Boolean category is given by the opposite of the category of \kappa -generated, \kappa -complete Boolean algebras and the \kappa -continuous homomorphisms between them.

It is not clear how to define a good probability theory on top of this—having continuum-sized unions seems to rule out many important measures like the Lebesgue measure.

Fritz and Lorenzin (Reference [fritz-lorenzin-abstractmeas-2025]) have recently described a category \mathsf {BaireMeas} of Baire measurable spaces (those arising as the Baire \sigma -algebra on a compact Hausdorff space X), as well as an associated Markov category of kernels \mathsf {BaireStoch}, which admits all (small) Kolmogorov products, and which contains \mathsf {BorelStoch} as a full subcategory.

Conjecture

\mathsf {BaireMeas} \hookrightarrow \mathsf {BaireStoch} is the initial Markov functor from \mathsf {BaireMeas} into a coinflip Markov category which preserves countable coproducts, pullbacks along coproduct inclusions, and all Kolmogorov products.

This seems amenable to the methods of this paper—what is missing is a concrete description of the general objects of \mathsf {BaireMeas} as limits of finite ones. However, a universal description of \mathsf {BaireMeas} itself seems elusive, since it is not Boolean—not every measurable injection between such spaces has a measurable image.

A general measurable map is difficult to represent computationally. It is therefore interesting to consider variations of this theorem which describe more computationally tractable situations. Note that every compactly supported measure on \mathbb {R}^k is the image of the uniform measure on 2^\omega under a continuous function, so many measures of interest can be represented in this way (if we work with the extended real line [-\infty , \infty ] instead, every probability measure can be represented).

Following the discussion above, the right question to ask seems to be, given a countably extensive Cartesian category \mathcal {C} (for example of topological spaces, or \omega -dcpos) with products up to a given size, for the free coinflip Markov category \overline {\mathcal {C}} so that the inclusion preserves countable coproducts, pullbacks along their inclusions and the given Kolmogorov products. It would be interesting to compare this with existing models of continuous probability, such as the category \mathsf {TychStoch} of Tychonoff spaces and continuous kernels introduced in Reference [markov-supports], and the category of \omega \mathrm {qbs}s and kernels introduced in Reference [vakar-kammar-staton-omega-qbs].

Problems that haunt me [efr-UJT4]

What is the connection between adjunctions (functional analysis) and adjunctions (category theory)

See Adjoint Functors Induced by Adjoint Linear Transformations: Given A: V \to U a map of inner product spaces, let S(A) : S(V)^\mathrm {op} \to S(U) be the contravariant mapping on the subspace posets which carries K \subset V to the set \{u \mid (u, Ak) =0 \forall k \in K\}. Then this assignment preserves adjunctions. Moreover if A, B are maps so that their images under this assignment are adjoint functors, they are adjoint as linear maps up to a scalar.

Chris Heunen's work on the category of Hilbert spaces.

Is there a good account of petri net gluing and the like as a tangency?

Is there a good tangency-type theory of hybrid systems, i.e those that have jumps at specific deterministic places?

Are the real numbers a limit of finite approximations (not colimit!) in some sense?

Assume-guarantee vs Nash

Is there a connection between assume-guarantee reasoning (satisfies x \star q \leq p \star q, p \star y \leq p \star q \Rightarrow x \star y \leq p \star q) and the Nash composition for open games x \star y \leq x \star q, x \star y \leq p \star y \Rightarrow x \star y \leq p \star q? They are "duals" to one another, is that anything?

Comparison of teleology

When talking about evolution, people often use what might be called "teleological reasoning". That is, an organism evolved to do X for purpose Y. This makes some amount of sense, but of course evolution is a particular dynamical system, which doesn't always follow naive game-theoretic logic. Can we say something formal about this, in the generality of mapping from dynamical systems to solution concepts in game theory? It would be interesting to say something like "evolution corresponds to X type of local optimimum composed according to tensor product Y (the Nash product or something else), given some abstract model of evolution as a dynamical system.

Stochastic type theory using Markov fibrations

There might also be space for Kolmogorov products here? Unclear. "Kolmogorov inductive types"

  1. Consider initial "Markov Comprehension Categories" of some sort as the syntactical models of this type theory.
  2. Figure out what sort of normalization proof would be desirable or necessary here.
  3. Distributive to get Bool and so on.
  4. Question is what are some actually interesting dependent types? Can add equality types with pullbacks and stuff.
  5. How does "the initial Markov etc etc" compare with a list of judgments?
  6. Can we expect any sort of normalization theorem here? Surely not in high generality.

Probabilistic programming with recursion in terms of initial Markov categories

Without the assumption of Boolean-ness, we can't define the map 2^\omega \to \mathbb {N} which takes the index of the first 1, hence we can't use this and the fact that an infinite set of coinflips always has a one to build up the rest of the measures, as in § [efr-AK18]. However, in a programming with recursion, this map is definable as a partial map. Can we use this to really build a minimal probability theory?

Probably important: Reference [vakar-kammar-staton-omega-qbs]

If we try working in these categories, we find we can't do the proof, since "infinitely many 1s" is not a continuous map (even if it's allowed to "not terminate" on the complement), but "at least one 1" is not independent of the prefix.

Can we do something with "CD category(partial markov), initial extensive and countably complete, plus traced for the coproduct"? This at least allows us to express the map that fails on all zeroes and else gives the index of the first 1.

Random thoughts on universal/synthetic probability theory [efr-RI1E]

The study of "probability theories with universal properties" (that is, Markov categories which are initial in some sense). There are two central types of questions:

  1. Can we give universal properties to existing Markov categories of interest?
  2. Can we characterize the initial Markov category with some given properties/generators?

This may be said to belong to "metatheory", that is the study of initial models of various type theories, although the existence of nondeterministic maps, and of infinitary (Kolmogorov) products, changes its nature somewhat.

See eg The Universal Property of Measure-Theoretic Probability (also on arxiv) for a result along these lines.

Lemma The Archimedean Probability Lemma [efr-ADS6]

Let \mathcal {C} be a distributive coinflip Markov category where the Kolmogorov product 2^\omega exists, let \chi : 2^\omega \to A be a deterministic map. Suppose there exist maps d: A \otimes A \to A and s: 2^\omega \to 2^\omega satisfying:

  1. For every finite N, \pi _{2^N}s : 2^\omega \to 2^\omega \to 2^N factors over some finite projection 2^\omega \to 2^M. Moreover each of these factorizations 2^M \to 2^N is given by a map of finite sets which has fibers of uniform size.
  2. \chi factors over every cofinite projection 2^\omega \to 2^{\omega _{>N}}.
  3. d(\chi (x), \chi (s(x))) = 1 as maps 2^\omega \to 2.
  4. d(x,x) = x.
Then \chi \circ f^\omega = 1, where f^\omega : I \to 2^\omega is the independent pairing of \omega -many coinflips.

Techniques like this allow you to control some subset of maps 2^K \to A being composed with coinflips. In the case of \mathsf {BorelStoch}, this appears to be enough as every measurable map is generated by the finitary ones and the countable disjunction \vee : 2^\omega \to 2 (by looking at \limsup : 2^\omega \to 2, which is necessarily less than \vee but can have the lemma apply to it, by taking d = \vee : 2^2 \to 2 and s to be the coordinatewise negation). Thus it appears that the initiality of \mathsf {Borel} is one of the key reasons why we can control all its maps interactions with coinflips without further axioms.

Since the map \limsup : 2^\omega \to 2 is not continuous, nor even continuous or computable in some weak sense (for example, the map 2^\omega \to \Omega , the space of truth values, is still not continuous, it is not even semidecidable, etc), we may want to study models of probability which prohibit this map. It is an interesting problem how to carry out the argument above without it. The objective would be to apply a proof to \vee : 2^\omega \to 2, whose composite with 2 \to \Omega is at least continuous (and it's semidecidable, etc). Since this is not independent of finite prefixes, we cannot apply the Kolmogorov 0-1 law in this case. We can apply Hewitt-Savage 0-1 law if we assume the Markov category is also causal.

It seems plausible that freely coinflip-complete Markov categories may always be causal, since we add "no extra equations", (similar to how multiplication is always injective in free monoids, but not in a generic monoid), but it is not obvious how to prove this.

Conjecture Preservation of Causality [efr-Z3WC]

Let \mathcal {C} be a Cartesian distributive category with countable products and let \mathcal {C} \to \bar {\mathcal {C}} be a (the) coinflip completion as a Markov category with countable Kolmogorov products. Then \bar {\mathcal {C}} is a causal Markov category.

Remark

I believe this is true without the Kolmogorov products, proven by characterizing the homset in terms of dyadic (finitary) distributions on maps.

Conjecture Description of Coinflip Completion [efr-U80H]

Let \mathcal {C} be a distributive Cartesian category with countable products. Then the morphisms A \to B of the coinflip completion with countable Kolmogorov products are given by equivalence classes of deterministic maps f: 2^\omega \otimes A \to B (which are morally identified with the map given by composing this with infinite independent coinflips).

The only nontrivial part is to show that these are stable under forming limiting maps into Kolmogorov products.

Perhaps an even simpler thing to start with would be whether these completions are positive, which is after all weaker than causality.

The lemma which is required in the proof of the Hewitt-Savage 0-1 law (which follows from causality, but is not equivalent to it, as far as I can see) is true whenever \mathcal {C}_\mathrm {det} has equalizers and the pullback

is preserved by the inclusion \mathcal {C}_\mathrm {det} \hookrightarrow \mathcal {C} (in \mathcal {C}_\mathrm {det} this pullback is equivalently an equalizer, but not in \mathcal {C}). In that case, given f,g deterministic (this is enough for the theorem), if (f,g)p = (f,f)p, then p factors over this equalizer, and it's then easy to see that f =_{p} g write (f,1)p as the factorization of p over the equalizer, the inclusion into X, and f, then observe that inclusion-f equals inclusion-p.

Hence given this level of limits, we can use the hewitt-savage argument to prove determinism for \vee : 2^\omega \to 2.

Much seems to revolve around some class of deterministic monos such that pullbacks along these exist and are preserved by \mathcal {C}_\mathrm {det} \hookrightarrow \mathcal {C}. We should give a "syntactical" understanding of this rather than saying "monos with property X also do this" (eg X = extremal or something).

From a programming/type theory point of view, the sensible thing is not to talk about deterministic morphisms, but to have a subsyntax for "pure" morphisms and speak of this category. And then have a statement that in the initial models all the deterministic maps are pure. This would necessitate modifying/rethinking the proof that \vee f^\omega = 1.

Conjecture Free Partial Markov Category [efr-A1R8]

Consider the CD-category which is initial so that

  1. The pure subcategory is countably extensive and countably complete
  2. The

A meta-principle, which you can hope to be true, is this: Given \hat {f}: 2^\omega \times A \to B in a Cartesian category representing f: A \to B in a coinflip completion, if f is deterministic, then there exists (at least one, but probably a set of full measure) b \in \{0,1\}^\omega (an actual bitstream, not in \mathcal {C}) so that \hat {f}(b,A) = f (and in particular f is already in the Cartesian category under consideration).

Lemma

Let \sigma _n : A \to \bigotimes B_i be a family of maps. Suppose for each finite subproduct, the marginal A \to \prod _{i \leq M} B_i is eventually constant, for n \geq n_M say. Suppose there is a (parameterized) measure P \to A so that \sigma _n \mu = \sigma _1 \mu for all n. Then \sigma _\infty \mu = \sigma _1 \mu also.

This is essentially the key part of my proofs in the universal property paper. The hard part in applying this obviously is proving that these maps exist, but also in proving that the limiting map actually exhibits the identity that you want. There we usually have to observe that it does on some measure-1 subset of the sample space, which is enough.

The specific pullbacks that have to be preserved is a bit unclear. It would be nice if they could all be deduced from the Kolmogorov property along with the assumption that decidable subsets/coproduct inclusions have this property.

On limits that are preserved by distribution monads

The property of Kolmogorov products is essentially that the cofiltered limit \prod _{i \in \mathbb {N}} X_i \cong \lim _{N} \prod _{i < N}X_i is preserved by the probability monad P, (or equivalently that it is preserved by the inclusion into the Kleisli category - this formulation has the advantage of making sense for Markov categories that are not monadic).

(Note that this does make sense for uncountable products also, quantifying instead over the poset of finite subsets of the indexing set). We can ask whether a general cofiltered limit is also preserved. Note that this cannot be true of all cofiltered limits, because an uncountable intersection of full-measure sets may be empty.

Let \lim _i A_i be a cofiltered limit. We can express it in terms of products and pullbacks, as the pullback of the diagram

(Here the bottom map is the diagonal, and the top carries (a_i) to (a_i, p^i_j(a_i)), where p are the maps in the diagram we are taking the colimit of). If this pullback is preserved by the probability monad, and the products here are carried to Kolmogorov products, one can show that the inverse limit is also preserved. (This pullback just expressed the limit as an equalizer - the point is that we can expect pullbacks like this to be preserved at least some of the time).

Thus we can not demand all Kolmogorov products (of all cardinalities) and that all pullbacks along monos (even split ones) are preserved by the functor. On the other hand, this also shows that, as soon as we have countable Kolmogorov products, we are pretty close to having T preserve all sequential cofiltered limits. This may be considered as an alternative axiom.

Note that we will usually demand that it preserve every pullback along a decidable subobject (that is, a coproduct inclusion). The class of subobjects whose classifying pullback (over * \xrightarrow {\top } \Omega ) is preserved by the probability monad is of great interest - this assumption implies it contains all the decidable subobjects. If we assume that countable cofiltered limits are preserved, we also get all the "co-semidecidable" ones, i.e those of the form \forall n. p(n) where p: \mathbb {N} \to 2 is a sequence of decidable propositions.

Is there a subobject version of the Kolmogorov or Hewitt-Savage 0-1 laws? It would state something like "given a subobject V \subseteq X^{\otimes \mathbb {N}} which is invariant under finite permutations, and an IID measure \mu : P \to X^\mathbb {N}, dots". Unclear what the statement should be - can't expect "either factors or factors over complement", since that requires decidability kind of.

There may be some way of stating this, in terms of whether two independent copies of the measure belong to the set or not. What I really want is: if two sets both have this property, then any measure which is concentrated on their union is also concentrated in one of them(??).

Possibly something like this would work for split monos, (maybe just by applying the splitting to the existing theorem). However the inclusion of streams with one 1 in all streams is not split (?).

But I think the map \sum _n \{b \in 2^\mathbb {N} \mid b_n = 1\} \to \{b \in 2^\mathbb {N} \mid \exists n: b_n=1\} does split (it's an epi) (under very mild assumptions, weaker than elementary topos+NNO). And I think this gives us a chance, since the former is a decidable subset of \mathbb {N} \times 2^\mathbb {N}.

Claude's proof that Giry on standard Borel spaces preserves all pullbacks

Here's the full writeup. The key structural insight is that the reduction is almost entirely formal — the only non-categorical input is disintegration of measures, used in one place at the end.

Setup

Let C = standard Borel spaces and Borel-measurable maps; equip it with the topology J generated by countable Borel partitions. Write \mathrm {Sh}(C,J) for the resulting topos; J is subcanonical, so representables are sheaves. Let P:C\to C be the Giry functor: PX is the standard Borel space of probability measures on X, and P(f)=f_* on a Borel map f. Let \tilde P:\mathrm {Sh}(C,J)\to \mathrm {Sh}(C,J) be the left Kan extension of ay\circ P along ay:C\to \mathrm {Sh}(C,J). Equivalently, \tilde P is the unique cocontinuous endofunctor of \mathrm {Sh}(C,J) whose value on representables is \tilde P(yX)=yPX. The single fact about P we use is: **(D) — Measurable disintegration.** For every Borel g:W\to T between standard Borel spaces, every T'\in C, and every kernel k_W:T'\to PW, the pushforward g_*k_W:T'\to PT admits a Borel-measurable disintegration: a family (k_W^{(t',x)}\in P(g^{-1}(x)))_{(t',x)\in T'\times T}, jointly Borel in (t',x), with k_W(t')=\int _T k_W^{(t',x)}\,d(g_*k_W(t'))(x)\quad \text {for every }t'. This is standard for standard Borel spaces (Kallenberg, *Foundations of Modern Probability*, Thm. 6.3 and surrounding).

Proposition

\tilde P preserves pullbacks along monomorphisms in \mathrm {Sh}(C,J): for every mono m:A\hookrightarrow B and every f:F\to B, the comparison \tilde P(F\times _B A)\longrightarrow \tilde P F\times _{\tilde P B}\tilde P A is an isomorphism.

Proof

Step 1 — Reduction to pullbacks of \mathrm {true} Every mono in a topos is the pullback of \mathrm {true}:1\to \Omega . Given m:A\hookrightarrow B classified by \chi :B\to \Omega and any f:F\to B, pullback pasting along \chi \circ f:F\to \Omega gives F\times _B A\;=\;F\times _B(B\times _\Omega 1)\;=\;F\times _\Omega 1. Suppose we have shown that \tilde P preserves the pullback X\times _\Omega 1\to X for every \chi :X\to \Omega . Note \tilde P 1=1 because 1=y(*) is representable and P(*)=*. Then, applying the hypothesis to both B\to \Omega and F\to \Omega and pasting, \tilde P(F\times _B A)=\tilde P(F\times _\Omega 1)=\tilde P F\times _{\tilde P\Omega }1=\tilde P F\times _{\tilde P B}(\tilde P B\times _{\tilde P\Omega }1)=\tilde P F\times _{\tilde P B}\tilde P A. So it suffices to prove: for every \chi :X\to \Omega , \tilde P preserves the pullback \chi ^{-1}(1)\to X. Step 2 — Reduction to mono into representable Write X=\mathrm {colim}_{(yT,b)\in \int X}yT as a colimit over its category of elements. Setting V:=\chi ^{-1}(1)\hookrightarrow X, universality of colimits in the topos gives V=\mathrm {colim}_T V_T, where V_T:=b^{-1}V\hookrightarrow yT. Suppose for every T\in C and every subsheaf U\hookrightarrow yT we have \tilde P U=\tilde P yT\times _{\tilde P\Omega }1. Then, using cocontinuity of \tilde P and universality of colimits in \mathrm {Sh}(C,J) (which lets us pull the pullback past the colimit), \tilde P V=\mathrm {colim}_T\tilde P V_T=\mathrm {colim}_T(\tilde P yT\times _{\tilde P\Omega }1)=(\mathrm {colim}_T\tilde P yT)\times _{\tilde P\Omega }1=\tilde P X\times _{\tilde P\Omega }1. So it suffices to prove the proposition when X=yT. Step 3 — The case U\hookrightarrow yT Fix T\in C and a subsheaf U\hookrightarrow yT, classified by \chi _U:yT\to \Omega . Then U(W)\subseteq C(W,T) is the set of g:W\to T such that g^*\chi _U=\mathrm {max}_W (the maximal sieve on W); equivalently, those g that factor through U as a sheaf map. The presheaf-level coend computing \tilde P: \tilde P F\;=\;a_!\left (\,\int ^{W\in C}F(W)\cdot yPW\,\right ). Sections of the presheaf coend at T' are equivalence classes of triples (W,\eta \in F(W),k\in C(T',PW)), where the equivalence is generated by basic moves: for each h:W_1\to W_2 in C, (W_1,F(h)\eta _2,k_1)\;\sim \;(W_2,\eta _2,P(h)_*k_1)\qquad (\eta _2\in F(W_2),\;k_1\in C(T',PW_1)). After sheafification, sections of \tilde P F at T' are presented by such triples, locally on a Borel partition of T', modulo local coend-equivalence. Specializing: - \tilde P yT(T')=yPT(T')=C(T',PT) — kernels. - \tilde P U(T') — locally, triples (W,g\in U(W),k_W:T'\to PW). - \tilde P\Omega (T') — locally, triples (W,\sigma \in \Omega (W),k_W). - \tilde P 1(T')=*. The map 1\to \tilde P\Omega sends * to the class [(W,\mathrm {max}_W,k_W)] for any choice of W and k_W (all such classes coincide via the unique map W\to *). The map \tilde P\chi _U:\tilde P yT\to \tilde P\Omega sends k\in C(T',PT) to [(T,\chi _U,k)]. The canonical comparison \Phi :\tilde P U\longrightarrow \tilde P yT\times _{\tilde P\Omega }1 sends (W,g,k_W) to g_*k_W\in C(T',PT). (Use the basic move along g:W\to T: (W,g,k_W)\sim (T,\mathrm {id}_T,g_*k_W), image g_*k_W.) The image lies in the pullback because g\in U(W) gives g^*\chi _U=\mathrm {max}_W, hence [(T,\chi _U,g_*k_W)]=[(W,\mathrm {max}_W,k_W)] which is the true class. We show \Phi is an isomorphism. Surjectivity of \Phi Let k\in C(T',PT) be a section of the pullback at T'. By definition this means: locally on T' (i.e., after passing to a Borel partition T'=\sqcup _i T'_i), the class [(T,\chi _U,k|_{T'_i})] in the presheaf coend equals the class of the true section. A *single span* witness for this equality is data (W,g:W\to T,k_W:T'_i\to PW) with g\in U(W) and g_*k_W=k|_{T'_i}: it gives (T,\chi _U,k|_{T'_i})\sim (W,g^*\chi _U=\mathrm {max}_W,k_W)\sim (*,\mathrm {max}_*,!) via the moves along g:W\to T (reverse) and W\to * (forward). A general witness is a finite zigzag of basic moves; we claim it can always be replaced by a single span. Inductively, two adjacent moves (W_1,\eta _1,k_1)\sim (W_3,\eta _3,k_3)\sim (W_2,\eta _2,k_2) along h_1:W_1\to W_3, h_2:W_2\to W_3 are replaced by a single span W_1\xleftarrow {p_1}W_1\times _{W_3}W_2\xrightarrow {p_2}W_2. The pullback exists in C (standard Borel is finitely complete). Setting \zeta :=F(p_1)\eta _1=F(p_2)\eta _2 (these agree because both equal F(h_1p_1)\eta _3=F(h_2p_2)\eta _3), we need a kernel \rho :T'_i\to P(W_1\times _{W_3}W_2) with (p_1)_*\rho =k_1 and (p_2)_*\rho =k_2 — given (h_1)_*k_1=k_3=(h_2)_*k_2. This is the coupling problem solved by (D); see the construction below. So locally on T', k admits a single-span presentation (W,g,k_W) with g\in U(W) and g_*k_W=k. The triple defines a local section of \tilde P U, and these glue (by sheafification) to a global section of \tilde P U mapping to k under \Phi . Injectivity of \Phi Suppose two local sections (W,g,k_W) and (W',g',k_{W'}) of \tilde P U at T' — both with g\in U(W), g'\in U(W') — satisfy g_*k_W=g'_*k_{W'}=k as kernels T'\to PT. We exhibit a single span witnessing their equality in \tilde P U(T'). Form W\times _T W'\in C (standard Borel as a closed Borel subset of W\times W'), with projections p:W\times _T W'\to W and p':W\times _T W'\to W'. We construct \rho :T'\to P(W\times _T W') with p_*\rho =k_W and p'_*\rho =k_{W'}. For each t'\in T', the measure \mu _{t'}:=g_*k_W(t')=g'_*k_{W'}(t')\in PT is well-defined. By (D), choose Borel-measurable disintegrations k_W(t')=\int _T k_W^{(t',x)}\,d\mu _{t'}(x),\qquad k_{W'}(t')=\int _T k_{W'}^{(t',x)}\,d\mu _{t'}(x), with k_W^{(t',x)}\in P(g^{-1}(x)) and k_{W'}^{(t',x)}\in P(g'^{-1}(x)). Set \rho (t')\;:=\;\int _T \bigl (k_W^{(t',x)}\otimes k_{W'}^{(t',x)}\bigr )\,d\mu _{t'}(x)\;\in \;P(W\times W'). The integrand at x is supported on g^{-1}(x)\times g'^{-1}(x)\subseteq W\times _T W', so \rho (t') is supported on W\times _T W' — view it as an element of P(W\times _T W'). Joint measurability of disintegrations gives Borel-measurability of \rho in t'. Verification of the projections: p_*\rho (t')=\int _T p_*\bigl (k_W^{(t',x)}\otimes k_{W'}^{(t',x)}\bigr )\,d\mu _{t'}(x)=\int _T k_W^{(t',x)}\,d\mu _{t'}(x)=k_W(t'), and symmetrically p'_*\rho =k_{W'}. Now apply basic moves. Along p:W\times _T W'\to W, with \eta _2=g: (W\times _T W',\;U(p)(g)=g\circ p,\;\rho )\;\sim \;(W,\;g,\;p_*\rho =k_W). Note g\circ p\in U(W\times _T W') because U is a sieve on T (closed under precomposition) and g\in U(W). Symmetrically along p': (W\times _T W',\;g'\circ p',\;\rho )\;\sim \;(W',\;g',\;k_{W'}). By the universal property of the pullback, g\circ p=g'\circ p' as maps W\times _T W'\to T, so the two left-hand triples coincide. Therefore (W,g,k_W) and (W',g',k_{W'}) represent the same local section of \tilde P U. \blacksquare

A couple of remarks worth flagging. The proof uses essentially nothing about the Giry monad beyond (D). Any functor F:C\to C on a finitely complete category, equipped with a "measurable disintegration" property of the same shape, will give an extension \tilde F preserving pullbacks along monos by exactly this argument. The structural ingredients are: (i) finite limits in C for forming W\times _T W', (ii) cocontinuity of \tilde F from the LKE construction, (iii) universality of colimits in the topos, (iv) (D) as the one analytic input. The mono-pullback hypothesis on P that we discussed earlier (P preserves g'^{-1}(W) for W\hookrightarrow T Borel) is the trivial special case of (D) where g is an inclusion: the disintegration is trivial because each fiber g^{-1}(x) is either empty or a single point. The general (D) is strictly stronger and is what's actually doing the work. The category-of-elements decomposition in Step 2 forces us to handle subsheaves U\hookrightarrow yT where U may be wildly non-Borel (Vitali, Bernstein, etc.), and the witnessing g:W\to T in the coend is then far from being a mono — disintegration over arbitrary g is unavoidable.

If we believe this theorem, then this is a sheaf topos model of probability where all pullbacks are preserved.

The Giry monad on sheaves on Borel preserves countable Kolmogorov products

To see this, recall the coend construction of Kan extensions: \tilde {P}(X)(T) = \int ^K X(K) \times \operatorname {\mathrm {Hom}}(T, PK). Let (X_i) be a sequential inverse limit of sheaves and write out: \int ^K \lim _i X_i(K) \times \operatorname {\mathrm {Hom}}(T, PK) \to \lim _i \int ^K X_i(K) \times \operatorname {\mathrm {Hom}}(T, PK)

An element of these coends consists of a (standard Borel) space K, a parameterized distrbution \mu : T \to PK, and a map \alpha : K \to X_i (that is, an element of X_i(K)). The equivalence relation identifies two elements if there exists a map f: K \to K' so that \alpha = f^*\alpha ' and \mu ' = P(f)\mu . A priori we have to take the reflective-transitive closure, i.e zigzags, but because of disintegrations, it suffices to consider spans. (Given kernels T \to PK, PK' that agree under two maps K,K' \to L, there exists at least one common lift of these measures to the pullback).

Thus if two elements are identified by the comparison map above, it means there exist spans K \leftarrow L_i \to K' witnessing the equality of their restriction to X_i for each i. Using Kolmogorov products in Borel, we can construct the product of all these L_i, then pull this back along the diagonal to K \times K', and use disintegration to construct a common lifting to all these L_i of the measures. This proves injectivity.

Conversely, let (K_i, \alpha _i, \mu _i) be a family on the right-hand side. At each step, let p_i: X_{i+1} \to X_i be the diagram maps. We have some equation between (K_i,\alpha _i,\mu _i) and (K_{i+1}, \alpha _{i+1}, \mu _{i+1}). Let it be witnessed by a span with apex M_{i+1}, \beta _{i+1}, \rho _{i+1}. Then we can just replace K_{i+1} with this - doing this inductively, we obtain a sequence M_{n+1} \to M_n \to \dots of equality witnesses. Taking the inverse limit of this (and analogously constructing the lift of the measures, again using the representable case) gives injectivity.

Instead of the Kolmogorov products axiom, we can consider the axiom that if a random truth value \phi satisfies \phi \leq \phi / 2 (defined in the obvious way in terms of the coinflip) then \not \phi (this should probably be a positive statement instead, although at the moment the right formulation escapes me). This relies on there existing a reasonable ordering on random truth values obviously. I'm attracted to this formulation because it's more finitary, and because it is reminiscent of the axiomatics for synthetic guarded domain theory.

I think this, like a lot of other stuff, is not a consequence of the Kolmogorov axiom but only admissible, that is it is true when \phi can be constructed inductively from the clopens in 2^\omega but not in full generality. However I don't know of any counterexample proving this, and as I've noted before, the combination of Kolmogorov products with any amount of nondeterminism seems to rule out certain types of "discontinuous maps".

Tao's old blog post on "probability sheaves" may be interesting. My old problem with that is that it only depends on which sets have probability one or zero. But the ideas developed here shows you can do a lot once you can prove that certain sets must have probability 1!

I have previously thought that "synthetic probability theory", unlike SDG (for example), doesn't involve any "exotic stuff" in the models (like the infinitesimals in SDG). (That is, we can construct models that have some exotic stuff if we want to, but we have no need of them or advantages in them). I think I have discovered at least one "exotic gadget" of this type. That is, take the sheaes on Borel spaces model above. Then "the union of all Lebesgue measure zero subsets of [0,1]" is an object which itself has measure zero in a relevant sense (maybe. Or at least, it has no positive measure..), which you could not construct classically.

Conjecture [efr-7N6B]

Let \mathcal {C} \to \mathcal {C}_s be a Markov promonad on an elementary topos which respects the natural numbers object, Kolmogorov products and pullbacks along monomorphisms. Then by Decidable Sampling, there is a natural transformation X \otimes X \otimes [0,1] \to X in \mathcal {C}_s (given by sampling from 2 according to the given probability, and then applying the resulting marginal).

Denote this operation (x,x',\lambda ) \mapsto x +_\lambda x'. This equips each object in \mathcal {C}_s with the structure of an internal convex space, in the sense that these operations satisfy the following equations:

x +_\lambda x = xx +_\lambda y = y +_{1 - \lambda } x(x +_\lambda y) +_\gamma z = x +_{\lambda \gamma } (y +_{\frac {\gamma (1 - \lambda )}{1 - \lambda \gamma }} z)

Proof

The first one is trivial, and the second is fairly straightforward - it suffices to observe that for all bitstreams b_i representing a real \alpha , \neg b_i is a representation of 1-\alpha .

The tricky seems to be impossible without some sort of hellish explicit representation.

Idea for proof of "convexity" for generic probabilities [efr-9LPI]

Consider the two ways of sampling one of three values:

  1. Sample t \in [0,1] uniformly, decide t < \lambda , \lambda < t < \lambda + \rho - \lambda \rho , \lambda + \rho - \lambda \rho < t
  2. Sample t_1, t_2 uniformly, decide t_1 < \lambda (if yes return a), else decide t_2 < \rho and return b or c

The latter corresponds to the formal convex combination a +_\lambda (b +_\rho c), whereas the former is an "unbiased" representation of the same thing. It seems clear that if we can prove their equivalence, we can prove the equivalence with (a + b) + c (whatever coefficients) also.

Now for dyadic rationals q,r, let f^{q,r} : 2^\mathbb {N} \to 3_\bot be the function parameterizing the unbiased choice, and let g^{q,r}: (2^\mathbb {N})^2 \to 3_\bot parameterize the "biased" choice. Note both of these are actually uniformly continuous and can be shown by finitary means to give the same distribution. Moreover we can construct a permutation \sigma ^{q,r} : 2^\mathbb {N} \to (2^\mathbb {N})^2 which witnesses this identity of probability.

Finally note that for generic reals, in both cases, we can write f^{\lambda ,rho}(s) = \sup _{q<\lambda , r<\rho }f^{q,r}(s) (choosing the ordering a > b > c on our choice set), and similarly for g. (This is because in both cases increasing \lambda or \rho can only move your choice c \to b or b \to a, not the other direction). Moreover (this is the nonobvious part) we can hopefully prove that there is a limiting permutation \sigma _{\lambda ,\rho }, which witnesses the identity between these limiting distributions (in the usual way, because we are with probability one in the fragment determined by some specific q,r, hence the two maps are equal because equal at that point).

We may be able to arrange it so we can just take the supremum (or maybe infimum) of the maps (this will only land in \Omega ^\mathbb {N}, but we can try to show that with probability one we actually land in 2^\mathbb {N})

We would like to prove, for example, a metatheorem like this: in the initial model, given a collection of sets U_q indexed by \mathbb {Q}_{< \alpha } for some Dedekind real \alpha , so that their probabilities are p_q, with q < r \Rightarrow U_q \subseteq U_r, then the probability of \cup _q U_q is \sup p_q.

It would actually be fine to just prove that in the initial model, distributions on finite sets n are represented by the internal Dedekind simplex \{t_1,\dots t_n \mid \sum _i t_i = 1\}. (We have already constructed [I hope] the supposed sampling map \Delta ^n \nrightarrow n and shown it is "homomorphism" in a suitable sense, but not proven it is universal [which should only hold under some initiality assumption])

Let \mu : \Gamma \nrightarrow [0,1] be a measure. Call e: \Gamma \to [0,1] an superexpected value of \mu if, for every finitary decomposition \mu = \sum t_i\mu _i, \sum _i t_i = 1, t_i: \Gamma \to [0,1], \mu _i : \Gamma \nrightarrow [0,1], and every set \alpha _i so that \mu _i \geq \alpha _i almost surely, we have e \geq \sum _i t_i \alpha _i. Analogously define subexpected values. Say an expected value is a super- and subexpected value. Question: is there always a unique expected value? Idea: try to turn this into a Dedekind cut.

Consistency: is it clear there is no measure on the empty set? Yes because we have a model.

Idea: bring metrics into the induction hypothesis. Cook up a model where objects are types, a regularly complete convex metric space where every point has distance at most one (then the coproducts of points put things at distance one), and a map from (generalized) points in this space to distributions. The tensor product of these guys should give us the right thing.

Formally an object should be a type X, a internal, complete barycentric algebra M (that is, an internal convex space, which is a metric space, complete as such, and where the metric satisfies the equations of a barycentric algebra) satisfying further d \leq 1, and for each context (that is, type) \Gamma a function \mathcal {C}(\Gamma , M) \to \mathcal {C}_s(\Gamma , X). (Here if we are working with a model where distributions are a monad, rather than just a promonad, we should restrict distribution types from occuring in the context). Furthermore we should ask for these to be equipped with a coalgebra structure for the completed tensor product on these things (which we have to show exist constructively!), and consider coalgebra homomorphisms (so that the Cartesian product on the distribution part becomes the tensor product).

We can derive "sequential completeness", that is the ability to take well-defined infinite sums, just from the convexity and the inverse limit property (we get a well-defined map from \lim _\leftarrow \Delta ^n to P(n^\infty ), distributions on the conats). I guess something similar would work for other profinite sets.

I guess the idea is we slowly build up a set of results like this, until algebras for this are "enough" that we can glue them to the space of distributions and get a model.

Let f,g be as in Idea for proof of "convexity" for generic probabilities . Then the limiting permutation \sigma ^{\alpha } : (2^\mathbb {N})^2 \to 2^\mathbb {N} can be written as the dyadic expansion of b : b < \alpha , \alpha + (1-\alpha )b' : b > \alpha , which exists because these numbers differ from every dyadic rational with probability 1. The challenge is to prove constructively that this dyadic expansion is uniform, i.e if the two input sequences are sampled uniformly, so is the output sequence. It is not even clear how to show that the first bit is fair, let alone that every prefix is fair.

Suppose we can define some reasonable probability monad on some topological topos (maybe pyknotic sets). Then we can attempt the following "glue model": an object is a type, a topological space and a map to the global sections (and maps must preserve this). (A map from the global points of the space to the global sections, or what?), and an analogous map from global points of PX to distributions in the initial model. (Maybe this latter is all we need).

nlab: locale of real numbers contains the following observation: if all reals are contstructible, then the interval has measure zero (since it can be covered by arbitrarily small unions of countable intervals). This can be avoided by working with the locale of reals, where even though every point can be covered, this cover doesn't necessarily cover the whole interval. This problem doesn't necessarily come up in minimal models as the one I've considered (since there this cover doesn't exist because it's not possible to construct it [every real is computable but this is not internally true]), but it still seems important to ponder what it means.

I have convinced myself that it is not possible to sample with Dedeking real probability using only the sequential cofiltered limits axiom (and thus also the "strong iterability" property, that if two measures approximate each other arbitrarily well they must be equal, must fail). I think this can be seen by considering a model \operatorname {\mathcal {S}\mathrm {h}}(\mathbb {R}, \operatorname {\mathcal {S}\mathrm {h}}(\mathsf {Borel})), where we recall that in sheaves on the reals, the Cauchy reals are the locally constant ones but the Dedekind reals are the continuous ones. I think this should carry a model where the distributions on a locally constant set themselves form a locally constant set. (Note that we add the measurable stuff to make it easier to construct any model at all, but I think this doesn't make a huge difference).

Thus the open questions are:

  1. Is the weak/sequential form of iterability still admissible?
  2. Does at least the proof of convexity for Cauchy reals go through (I think it does)? (And also sampling with Cauchy probability, for that matter)
  3. Is there a modified version of the Kolmogorov axiom which lets you sample Dedekind reals? I don't see how at this moment. (Of course, you can add the strong iterability condition as a further axiom.)
  4. Can you sample with Escardo-Simpson probability? Recall that these are the Cauchy closure of the rationals inside the Dedekind reals, i.e not just limits of rational sequences, but limits of sequences of such, iterated. This follows from iterability by the work of Escardo-Simpson.
  5. If you can sample with probability p_i, can you sample with probability \sum _i 2^i 1/p_i? Note that there is an obvious way to do something that should be this, but I don't know if we can prove this is equal to the probability of being less that that number (without countable choice). And if yes, does this imply the previous? (In other words, given a Cauchy sequence of reals, can you write their limit as a sum of (say) rational combinations of them, without using countable choice?)

For this last step, here's the loose argument that given a Cauchy sequence of rationals we can build a sampling plan:

  1. Let q_n be the sequence, supposing q_n within 1/2^n of the limit.
  2. Consider q_3 (which is within 1/8). It's in either [ 0, 3/8 ), [3/8, 5/8], ( 5/8, 1 ]. Note that this is decidable. We can either choose the first thing in the sum to be 0 (since it's definitely less than 1/2), 1/2 (since it's at least 1/4 and at most 3/4 in the middle case) or 1.
  3. Then we iterate this.
Note that the second step here fails if we have a Cauchy sequence of reals (even Cauchy reals). We can find a cover of intervals so that each one has a valid choice, but not a disjoint decidable cover like this, so we can't set up a unique decision for each possible case.

You can try to take (q_n - 1/2^n) for some n as the first term in the sum. The problem with this is that if it's less than zero, we just know the limit might be zero (so we can't put a positive number in the sum). If it's less than zero obviously we can just put zero (since the whole thing is less than 1/2 then), but this is not decidable, and if there are multiple options we have to choose one.

Conjecture A completeness conjecture [efr-V74O]

Consider an initial "model of probability theory" in the sense of § [efr-AK18], call it \mathcal {C}. That is, an initial (pre-)Markov category with (internal?) countable Kolmogorov products, coproducts, extensive, with coinflip. Let \mathcal {C} \to \mathsf {QBS}_P be the unique functor, where P is the left Kan extension probability monad on \mathsf {QBS}. (Possibly, consider \mathsf {Sh(Borel)} instead). Then the map \mathcal {C}(1,2^\mathbb {N}) \to |P(2^\mathbb {N})| is injective. In other words any two "constructible" measures are provably identical using the axioms if and only if they represent the same actual measure.

Remark

It actually suffices to verify this for P(2^N), since both of these are limits of these.

Thoughts

I believe P is the initial monad on \mathsf {Sh(Borel)} satisfying this, which should help. This seems to be the sort of problem where tait computability methods actually help (since it is about proving injectivity of a particular universal "interpretation" functor).

Consider the initial model of this, glued to \mathsf {Sh(Borel)}. Given a map X \to \Gamma (A) where A a "type" and X a space, if A \to K where K finite and discrete, then we get X \to K. Say that a distribution here is a distribution on A (in the initial model), a distribution on X, so that for every such map the internal distribution of K is the normal form of the image measure.

Update

I now think this is false. Rather elements of \mathcal {C}(1,2) should be constructible reals in some sense, and there should be constructible reals which are equal but not provably so (maybe?). For example, given a program which loops forever, but not provably so, consider the real which has a zero for every step until it terminates, then a 1. This is a computable real but not provably equal to zero (but it is zero). (Here provably refers to the internal logic of this initial topos - it should provably terminate in the metatheory.)

Quantitative logic

Specifically, what does the model theory look like, especially in terms of higher-order logic and categorical models.

Reference A convenient category for higher-order probability theory [heunen-kammar-staton-yang-2017]

Introduces quasi-Borel spaces: sets equipped with a class of "admissible random elements" from \RR , closed under precomposition with measurable maps and under countable measurable case-splits. The category is cartesian closed with a commutative probability monad, fixing the failure of cartesian closure of \Meas . Relevant here for the site it implicitly certifies: quasi-Borel spaces are the concrete sheaves on the category of standard Borel spaces equipped with the coverage of countable measurable partitions, so the full topos of sheaves on that site is a natural "measurable-space-like" Grothendieck topos in which QBS embeds. Used downstream in Vákár–Kammar–Staton.

@inproceedings{heunen-kammar-staton-yang-2017, title={A convenient category for higher-order probability theory}, booktitle={Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}, author={Heunen, Chris and Kammar, Ohad and Staton, Sam and Yang, Hongseok}, year={2017}}