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.

Context

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.)