I’m interested in algorithmically random sequences. I feel like they should offer some sort of canonical object in the topos [\mathsf{lott},\mathcal{y}]\text{-}\mathbf{Coalg}. Let me explain.
The polynomial monad \mathsf{lott}:\mathbf{Set}\to\mathbf{Set} is a lot like the distributions monad \Delta:\mathbf{Set}\to\mathbf{Set} given by
\quad\Delta(X)\coloneqq\{p\colon X\to[0,1]\mid 1=\sum_{x:X}p(x)\textnormal{ and } p \textnormal{ has finite support}\}.
Saying that p has finite support means:
\quad \exists X'\subseteq X, X' \textnormal{ finite}, p(x)>0\implies x\in X'.
Both \mathsf{lott} and \Delta are monads on \mathbf{Set}.
The difference between \mathsf{lott} and \Delta is that an element of \mathsf{lott}(X) in some sense chooses its support:
\quad\mathsf{lott}(X)\coloneqq\sum_{N:\mathbb{N}}\Delta_NX^N.
It chooses a set N of tickets and a probability distribution p\colon N\to[0,1] on those tickets, and then for each ticket, it assigns an element of X. The “lottery” terminology comes from Von Neumann-Morgenstern. Another difference is that \mathsf{lott} is a polynomial functor. A position of \mathsf{lott} is a lottery (N,p), and a direction there is a choice n:N of ticket.
Polynomial functors form a monoidal closed category (in infinitely many different ways, but we’ll focus on one) where the monoidal product \otimes is given by Day convolution of (\times)\colon\mathbf{Set}\times\mathbf{Set}\to\mathbf{Set}, i.e. p\otimes q is universal among polynomials equipped with a natural map
\quad p(A)\times q(B)\to (p\otimes q)(A\times B)
for any sets A,B.
But in this post, we’re interested in the corresponding internal hom [-,-]. For any p,q, the polynomial [p,q] is the universal object for which there are natural maps
\quad [p,q](A)\times p(B)\to q(A\times B).
But it’s a polynomial, and I usually think of it in those terms, i.e.\ as given by the following formula:
\quad [p,q]\coloneqq\sum_{\varphi\colon p\to q}\mathcal{y}^{\sum_{I:p(1)}q[\varphi(I)]}.
So what is [\mathsf{lott},\mathcal{y}]? Its positions are polynomial maps \mathsf{lott}\to\mathcal{y} and its direction-set is always the set \mathsf{lott}(1) of lotteries:
\quad[\mathsf{lott},\mathcal{y}]\coloneqq\sum_{\varphi\colon\mathsf{lott}\to\mathcal{y}}\mathcal{y}^{\mathsf{lott}(1)}.
A position of this polynomial makes a choice of “winning” ticket for every lottery. A direction tells us which lottery (N,p):\mathsf{lott}(1) is chosen.
We should be able to get a canonical coalgebra on [\mathsf{lott},\mathcal{y}] by using random sequences. A coalgebra f\colon S\to p(S) of a polynomial functor p can be understood as a discrete-time open dynamical system that outputs positions of p and inputs directions of p. The collection of p-coalgebras and maps between them forms a topos.
In the case that p=[\mathsf{lott},\mathcal{y}], any dynamical system would output a choice of winning ticket for each lottery; then given a choice of lottery, it would update its state. So in the current state it would pick a winning ticket for the lottery (.7, .2, .1) and a winning ticket for the lottery (.9,.1), etc. It picks one ticket for each lottery. Then you tell it which lottery you want to unveil, and the state updates.
But are all choices of systematic ticket choosing equally good? Clearly not: we would not want a system that always chose the first ticket, or one that chose the least likely ticket; we want one that follows the distribution! Moreover, if the distribution was (.5, .5), we wouldn’t want to get the sequence (0,1,0,1,0,1,0,1,\ldots), because that doesn’t feel like a lottery. In the sense of algorithmically-random sequences, it’s not one because it’s compressible.
So I believe there is a special object in the topos [\mathsf{lott},\mathcal{y}]\text{-}\mathbf{Coalg}. We might as well make it be subterminal, meaning that it is just a set of behaviors: no two states act the same way; this just makes it easier to conceive of. How would you make this canonical object? Well, you could take it to be all algorithmically random sequences for each lottery.
In other words, at any state, it outputs a choice of winning ticket for each lottery. When a lottery is chosen, we keep all the other lottery winners the same and update the winning ticket for that lottery. Thus for any sequence of lotteries, we get a sequence of winning tickets. This should be algorithmically random, and every algorithmically random way of doing this should be in our coalgebra.
Inside the topos [\mathsf{lott},\mathcal{y}]\text{-}\mathbf{Coalg}, there really aren’t that many objects that should be considered "good’'. Any object repeatedly chooses a winning ticket for each lottery, and if the sequence of such didn’t follow the rules of randomness, it would violate the semantics of a lottery. In other words, we can tell ourselves what the notion of lottery means by choosing a coalgebra.
But can we think of any mathematical sense in which such an object is canonical, or satisfies a universal property, or is in any way distinguished?